diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 20d0e2dd00..3bb41568dc 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -9,14 +9,16 @@
 
 - in `realfun.v`:
   + instance `is_derive1_sqrt`
+
 - in `mathcomp_extra.v`:
   + lemmas `subrKC`, `sumr_le0`, `card_fset_sum1`
 
 - in `functions.v`:
   + lemmas `fct_prodE`, `prodrfctE`
 
-- in `exp.v:
+- in `exp.v`:
   + lemma `norm_expR`
+
 - in `hoelder.v`
   + lemma `hoelder_conj_ge1`
 
@@ -35,17 +37,39 @@
   + lemmas `closed_Fsigma`, `Gdelta_measurable`, `Gdelta_subspace_open`,
     `irrational_Gdelta`, `not_rational_Gdelta`
 
+- in `constructive_ereal.v`:
+  + lemma `expe0`, `mule0n`, `muleS`
+
+- in `exp.v`:
+  + lemmas `expeR_eqy`
+  + lemmas `lt0_powR1`, `powR_eq1`
+  + definition `lne`
+  + lemmas `le0_lneNy`, `lne_EFin`, `expeRK`, `lneK`, `lneK_eq`, `lne1`, `lneM`, 
+    `lne_inj`, `lneV`, `lne_div`, `lte_lne`, `lee_lne`, `lneXn`, `le_lne1Dx`, 
+    `lne_sublinear`, `lne_ge0`, `lne_lt0`, `lne_gt0`, `lne_le0`
+  + lemma `lne_eq0`
+
+- in `charge.v`:
+  + definition `copp`, lemma `cscaleN1`
+
 ### Changed
 
 - moved from `pi_irrational.v` to `reals.v` and changed
   + definition `rational`
 
+- in `constructive_ereal.v`:
+  + lemma `mulN1e`
+
 ### Renamed
 
 - in `lebesgue_stieltjes_measure.v`:
   + `cumulativeNy0` -> `cumulativeNy`
   + `cumulativey1` -> `cumulativey`
 
+- in `exp.v`:
+  + `ltr_expeR` -> `lte_expeR`
+  + `ler_expeR` -> `lee_expeR`
+
 ### Generalized
 
 - in `functions.v`
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index 0e8ea79d9e..5fa11a3bbd 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -726,8 +726,12 @@ Proof. by elim: n => //= n ->. Qed.
 Lemma enatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.
 Proof. by elim: n => //= n ->. Qed.
 
+Lemma mule0n x : x *+ 0 = 0. Proof. by []. Qed.
+
 Lemma mule2n x : x *+ 2 = x + x. Proof. by []. Qed.
 
+Lemma expe0 x : x ^+ 0 = 1. Proof. by []. Qed.
+
 Lemma expe2 x : x ^+ 2 = x * x. Proof. by []. Qed.
 
 Lemma leeN2 : {mono @oppe R : x y /~ x <= y}.
@@ -862,6 +866,9 @@ Lemma addeC : commutative (S := \bar R) +%E. Proof. exact: addrC. Qed.
 
 Lemma adde0 : right_id (0 : \bar R) +%E. Proof. exact: addr0. Qed.
 
+Lemma muleS x n : x *+ n.+1 = x + x *+ n.
+Proof. by case: n => //=; rewrite adde0. Qed.
+
 Lemma add0e : left_id (0 : \bar R) +%E. Proof. exact: add0r. Qed.
 
 Lemma addeA : associative (S := \bar R) +%E. Proof. exact: addrA. Qed.
@@ -1266,13 +1273,13 @@ Proof. by move=> rreal; rewrite muleC real_mulrNy. Qed.
 
 Definition real_mulr_infty := (real_mulry, real_mulyr, real_mulrNy, real_mulNyr).
 
-Lemma mulN1e x : - 1%E * x = - x.
+Lemma mulN1e x : (- 1%E) * x = - x.
 Proof.
-rewrite -EFinN /mule/=; case: x => [x||];
-  do ?[by rewrite mulN1r|by rewrite eqe oppr_eq0 oner_eq0 lte_fin ltr0N1].
+by case: x => [r| |]/=;
+  rewrite /mule ?mulN1r// eqe oppr_eq0 oner_eq0/= lte_fin oppr_gt0 ltr10.
 Qed.
 
-Lemma muleN1 x : x * - 1%E = - x. Proof. by rewrite muleC mulN1e. Qed.
+Lemma muleN1 x : x * (- 1%E) = - x. Proof. by rewrite muleC mulN1e. Qed.
 
 Lemma mule_neq0 x y : x != 0 -> y != 0 -> x * y != 0.
 Proof.
@@ -1284,7 +1291,7 @@ Qed.
 Lemma mule_eq0 x y : (x * y == 0) = (x == 0) || (y == 0).
 Proof.
 apply/idP/idP => [|/orP[] /eqP->]; rewrite ?(mule0, mul0e)//.
-by apply: contraTT => /norP[]; apply: mule_neq0.
+by apply: contraTT => /norP[]; exact: mule_neq0.
 Qed.
 
 Lemma mule_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x * y.
diff --git a/theories/charge.v b/theories/charge.v
index e635c77927..32fd4a16ba 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -43,7 +43,9 @@ From mathcomp Require Import lebesgue_measure lebesgue_integral.
 (*                              non-measurable sets                           *)
 (*                     czero == zero charge                                   *)
 (*               cscale r nu == charge nu scaled by a factor r : R            *)
-(*          charge_add n1 n2 == the charge corresponding to the sum of        *)
+(*                   copp nu == the charge corresponding to the opposite of   *)
+(*                              the charges nu                                *)
+(*                cadd n1 n2 == the charge corresponding to the sum of        *)
 (*                              charges n1 and n2                             *)
 (* charge_of_finite_measure mu == charge corresponding to a finite measure mu *)
 (* ```                                                                        *)
@@ -440,6 +442,38 @@ move=> /negbTE c0 munu E mE /eqP; rewrite /cscale mule_eq0 eqe c0/=.
 by move=> /eqP/munu; exact.
 Qed.
 
+Section charge_opp.
+Local Open Scope ereal_scope.
+Context d (T : measurableType d) (R : realType).
+Variables (nu : {charge set T -> \bar R}).
+
+Definition copp := \- nu.
+
+Let copp0 : copp set0 = 0.
+Proof. by rewrite /copp charge0 oppe0. Qed.
+
+Let copp_finite A : measurable A -> copp A \is a fin_num.
+Proof. by move=> mA; rewrite fin_numN fin_num_measure. Qed.
+
+Let copp_sigma_additive : semi_sigma_additive copp.
+Proof.
+move=> F mF tF mUF; rewrite /copp; under eq_fun.
+  move=> n; rewrite sumeN; last first.
+    by move=> p q _ _; rewrite fin_num_adde_defl// fin_num_measure.
+  over.
+exact/cvgeN/charge_semi_sigma_additive.
+Qed.
+
+HB.instance Definition _ := isCharge.Build _ _ _ copp
+  copp0 copp_finite copp_sigma_additive.
+
+End charge_opp.
+
+Lemma cscaleN1 {d} {T : ringOfSetsType d} {R : realFieldType}
+    (nu : {charge set T -> \bar R}) :
+  cscale (-1) nu = \- nu.
+Proof. by rewrite /cscale/=; apply/funext => x; rewrite mulN1e. Qed.
+
 Section charge_add.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType).
@@ -944,7 +978,7 @@ Local Definition cjordan_neg : {charge set T -> \bar R} :=
   cscale (-1) (crestr0 nu mN).
 
 Lemma cjordan_negE A : cjordan_neg A = - crestr0 nu mN A.
-Proof. by rewrite /= /cscale/= EFinN mulN1e. Qed.
+Proof. by rewrite /= cscaleN1. Qed.
 
 Let positive_set_cjordan_neg E : 0 <= cjordan_neg E.
 Proof.
@@ -970,7 +1004,7 @@ Lemma jordan_decomp (A : set T) : measurable A ->
   nu A = cadd jordan_pos (cscale (-1) jordan_neg) A.
 Proof.
 move=> mA.
-rewrite /cadd cjordan_posE /= /cscale EFinN mulN1e cjordan_negE oppeK.
+rewrite /cadd cjordan_posE/= cscaleN1 cjordan_negE oppeK.
 rewrite /crestr0 mem_set// -[in LHS](setIT A).
 case: nuPN => _ _ <- PN0; rewrite setIUr chargeU//.
 - exact: measurableI.
@@ -1045,7 +1079,7 @@ Lemma abse_charge_variation d (T : measurableType d) (R : realType)
   measurable A -> `|nu A| <= charge_variation PN A.
 Proof.
 move=> mA.
-rewrite (jordan_decomp PN mA) /cadd/= /cscale/= mulN1e /charge_variation.
+rewrite (jordan_decomp PN mA) /cadd/= cscaleN1 /charge_variation.
 by rewrite (le_trans (lee_abs_sub _ _))// !gee0_abs.
 Qed.
 
@@ -2034,8 +2068,7 @@ exists (fp \- fn); split; first by move=> x; rewrite fin_numB// fpfin fnfin.
   exact: integrableB.
 move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//;
   [|exact: (integrableS measurableT)..].
-rewrite -fpE ?inE// -fnE ?inE//= /cadd/= jordan_posE jordan_negE.
-by rewrite /cscale EFinN mulN1e.
+by rewrite -fpE ?inE// -fnE ?inE//= /cadd/= cscaleN1.
 Qed.
 
 Definition Radon_Nikodym : T -> \bar R :=
diff --git a/theories/ereal.v b/theories/ereal.v
index 57d721ac28..f2401270d2 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -1066,7 +1066,7 @@ Definition lt_expandRL := monoRL_in
 Lemma contract_eq0 x : (contract x == 0%R) = (x == 0).
 Proof. by rewrite -(can_eq contractK) contract0. Qed.
 
-Lemma contract_eqN1 x : (contract x == -1) = (x == -oo).
+Lemma contract_eqN1 x : (contract x == (- 1)%R) = (x == -oo).
 Proof. by rewrite -(can_eq contractK). Qed.
 
 Lemma contract_eq1 x : (contract x == 1%R) = (x == +oo).
@@ -1352,7 +1352,7 @@ move: reN1; rewrite eq_sym neq_lt => /orP[reN1|reN1].
       rewrite (@lt_le_trans _ _ 1%R) // ?lerDr//.
       by rewrite (le_lt_trans (ler_norm _))// contract_lt1.
     have ? : (`|contract r%:E + e%:num| < 1)%R.
-      rewrite ltr_norml re1 andbT -(addr0 (-1)) ler_ltD //.
+      rewrite ltr_norml re1 andbT -(addr0 (- 1)%R) ler_ltD //.
       by move: (contract_le1 r%:E); rewrite ler_norml => /andP[].
     pose e' : R := Num.min
       (r - fine (expand (contract r%:E - e%:num)))%R
diff --git a/theories/exp.v b/theories/exp.v
index f1358bd12a..e8b017da29 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -21,7 +21,8 @@ From mathcomp Require Import realfun interval_inference convex.
 (*   pseries_diffs f i == (i + 1) * f (i + 1)                                 *)
 (*                                                                            *)
 (*             expeR x == extended real number-valued exponential function    *)
-(*                ln x == the natural logarithm                               *)
+(*                ln x == the natural logarithm, in ring_scope                *)
+(*               lne x == the natural logarithm, in ereal_scope               *)
 (*              s `^ r == power function, in ring_scope (assumes s >= 0)      *)
 (*              e `^ r == power function, in ereal_scope (assumes e >= 0)     *)
 (*          riemannR a == sequence n |-> 1 / (n.+1) `^ a where a has a type   *)
@@ -471,7 +472,7 @@ Proof. by rewrite expRD expRN. Qed.
 Lemma ltr_expR : {mono (@expR R) : x y / x < y}.
 Proof.
 move=> x y.
-by  rewrite -[in LHS](subrK x y) expRD ltr_pMl ?expR_gt0 // expR_gt1 subr_gt0.
+by rewrite -[in LHS](subrK x y) expRD ltr_pMl ?expR_gt0 // expR_gt1 subr_gt0.
 Qed.
 
 Lemma ler_expR : {mono (@expR R) : x y / x <= y}.
@@ -628,6 +629,9 @@ Proof. by case: x => //= r; rewrite lte_fin expR_gt0. Qed.
 Lemma expeR_eq0 x : (expeR x == 0) = (x == -oo).
 Proof. by case: x => //= [r|]; rewrite ?eqxx// eqe expR_eq0. Qed.
 
+Lemma expeR_eqy x : (expeR x == +oo) = (x == +oo).
+Proof. by case: x. Qed.
+
 Lemma expeRD x y : expeR (x + y) = expeR x * expeR y.
 Proof.
 case: x => /= [r| |]; last by rewrite mul0e.
@@ -645,7 +649,7 @@ case : x => //= [r|]; last by rewrite addeNy.
 by rewrite -EFinD !lee_fin; exact: expR_ge1Dx.
 Qed.
 
-Lemma ltr_expeR : {mono expeR : x y / x < y}.
+Lemma lte_expeR : {mono expeR : x y / x < y}.
 Proof.
 move=> [r| |] [s| |]//=; rewrite ?ltry//.
 - by rewrite !lte_fin ltr_expR.
@@ -653,7 +657,7 @@ move=> [r| |] [s| |]//=; rewrite ?ltry//.
 - by rewrite lte_fin expR_gt0 ltNye.
 Qed.
 
-Lemma ler_expeR : {mono expeR : x y / x <= y}.
+Lemma lee_expeR : {mono expeR : x y / x <= y}.
 Proof.
 move=> [r| |] [s| |]//=; rewrite ?leey ?lexx//.
 - by rewrite !lee_fin ler_expR.
@@ -677,6 +681,10 @@ by rewrite lte_fin => /expR_total[y <-]; exists y%:E.
 Qed.
 
 End expeR.
+#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed `lte_expeR`")]
+Notation ltr_expeR := lte_expeR (only parsing).
+#[deprecated(since="mathcomp-analysis 1.13.0", note="renamed `lee_expeR`")]
+Notation ler_expeR := lee_expeR (only parsing).
 
 Section Ln.
 Variable R : realType.
@@ -771,7 +779,7 @@ Proof.
 by move=> x_gt1; rewrite -ltr_expR expR0 lnK // qualifE/= (lt_trans _ x_gt1).
 Qed.
 
-Lemma ln_le0 (x : R) : x <= 1 -> ln x <= 0.
+Lemma ln_le0 x : x <= 1 -> ln x <= 0.
 Proof.
 have [x0|x0 x1] := leP x 0; first by rewrite ln0.
 by rewrite -ler_expR expR0 lnK.
@@ -1118,9 +1126,142 @@ move=> x_gt0; split.
 by rewrite -derive1E powR_derive1// in_itv andbT.
 Qed.
 
+Lemma lt0_powR1 x p : x < 0 -> x `^ p = 1.
+Proof.
+by move=> x0; rewrite /powR lt_eqF// (ln0 (ltW x0)) mulr0 expR0.
+Qed.
+
+Lemma powR_eq1 x p : (x `^ p == 1) = [|| (x == 1), (x < 0) | (p == 0)].
+Proof.
+have [->/=|x1] := eqVneq x 1; first by rewrite powR1 eqxx.
+have [->|p0]/= := eqVneq p 0; first by rewrite powRr0 eqxx orbT.
+have [x0|x0|->]/= := ltgtP x 0; first by rewrite lt0_powR1// eqxx.
+- rewrite /powR (gt_eqF x0)// -expR0; apply/negP => /eqP/expR_inj/eqP.
+  rewrite mulf_eq0 (negbTE p0)/= -ln1 => /eqP/ln_inj => /(_ _ _)/eqP.
+  by rewrite (negbTE x1) falseE; apply => //; rewrite posrE.
+- by rewrite powR0// eq_sym oner_eq0.
+Qed.
+
 End PowR.
 Notation "a `^ x" := (powR a x) : ring_scope.
 
+Section Lne.
+Variable R : realType.
+Implicit Types (x : \bar R) (r : R).
+Local Open Scope ereal_scope.
+
+Definition lne x :=
+  match x with
+  | r%:E => if (r <= 0)%R then -oo else (ln r)%:E
+  | +oo => +oo
+  | -oo => -oo
+  end.
+
+Lemma le0_lneNy x : x <= 0 -> lne x = -oo.
+Proof.
+by move: x => [r| |]//=; case: ifPn => //; rewrite lee_fin => /negbTE ->.
+Qed.
+
+Lemma lne_EFin r : (0 < r)%R -> lne (r%:E) = (ln r)%:E.
+Proof. by move=> /=; case: ifPn => //; rewrite leNgt => /negbTE ->. Qed.
+
+Lemma expeRK : cancel expeR lne.
+Proof. by case=> //=[x|]; rewrite ?lexx// leNgt expR_gt0/= expRK. Qed.
+
+Lemma lneK : {in `[0, +oo], cancel lne (@expeR R)}.
+Proof.
+move=> [r|//|//]; rewrite in_itv => //= /andP[]; rewrite lee_fin.
+by rewrite le_eqVlt => /predU1P[<- _|r0 _]; rewrite ?lexx// leNgt r0/= lnK.
+Qed.
+
+Lemma lneK_eq x : (expeR (lne x) == x) = (0 <= x).
+Proof.
+move: x => [r| |]//=; last by rewrite eqxx leey.
+case: ifPn => [r0|]/=; first by rewrite eq_le !lee_fin r0 andbT.
+by rewrite -ltNge => r0; rewrite eqe lnK_eq lee_fin le_eqVlt r0 orbT.
+Qed.
+
+Lemma lne1 : lne 1 = 0. Proof. by rewrite lne_EFin//= ln1. Qed.
+
+Lemma lneM : {in `]0, +oo] &, {morph lne : x y / x * y >-> x + y}}.
+Proof.
+move=> x y /[!in_itv]/= /[!@leey R]/= /[!andbT] x0 y0.
+by apply: expeR_inj; rewrite expeRD !lneK// in_itv/= leey ltW ?mule_gt0.
+Qed.
+
+Lemma lne_inj : {in `[0, +oo] &, injective lne}.
+Proof. by move=> x y /lneK {2}<- /lneK {2}<- ->. Qed.
+
+Lemma lneV r : (0 < r)%R -> lne r^-1%:E = - lne (r%:E).
+Proof. by move=> r0; rewrite !lne_EFin ?gt_eqF ?invr_gt0// lnV. Qed.
+
+Lemma lne_div : {in `]0, +oo] &, {morph lne : x y / x / y >-> x - y}}.
+Proof.
+move=> [x| |] [y| |]//; rewrite !in_itv/= !leey !andbT ?lte_fin => x0 y0.
+- rewrite inver// !gt_eqF//= pmulr_rle0// invr_le0 leNgt y0/=.
+  by rewrite leNgt x0/= ln_div.
+- by rewrite mulr0 lexx leNgt x0/=.
+- by rewrite inver !gt_eqF// leNgt y0/= gt0_mulye// lte_fin invr_gt0.
+- by rewrite invey mule0/= lexx.
+Qed.
+
+Lemma lte_lne : {in `[0, +oo] &, {mono lne : x y / x < y}}.
+Proof. by move => x y x0 y0; rewrite -lte_expeR !lneK. Qed.
+
+Lemma lee_lne : {in `[0, +oo] &, {mono lne : x y / x <= y}}.
+Proof. by move=> x y x_gt0 y_gt0; rewrite -lee_expeR !lneK. Qed.
+
+Lemma lneXn n x : 0 < x -> lne (x ^+ n) = lne x *+ n.
+Proof.
+elim: n x => [x x0|n ih x x0]; first by rewrite expe0 mule0n lne1.
+by rewrite expeS lneM ?ih ?muleS// in_itv/= ?expe_gt0// ?x0/= leey.
+Qed.
+
+Lemma le_lne1Dx x : - 1%E <= x -> lne (1 + x) <= x.
+Proof.
+move=> ?; rewrite -lee_expeR lneK ?expeR_ge1Dx //.
+by rewrite in_itv //= leey andbT addrC -(oppeK 1) sube_ge0.
+Qed.
+
+Lemma lne_sublinear x : x \is a fin_num -> lne x < x.
+Proof.
+move=> xfin; have [x0|x0] := leP x 0.
+  by rewrite le0_lneNy// ltNye_eq xfin.
+have ? : (0 < fine x)%R by rewrite fine_gt0// x0/= ltey_eq xfin.
+by rewrite -(fineK xfin) lne_EFin// lte_fin ln_sublinear.
+Qed.
+
+Lemma lne_ge0 x : (0 <= lne x) = (1 <= x).
+Proof.
+apply/idP/idP.
+  case: x => [r||]//=; last by move=> _; rewrite leey.
+  case: ifPn => //; rewrite -ltNge lee_fin => r0.
+  by rewrite -ln1 ler_ln// posrE.
+case: x => [r||]//; rewrite ?leey// lee_fin => r1.
+by rewrite lne_EFin// ?(lt_le_trans _ r1)// lee_fin ln_ge0.
+Qed.
+
+Lemma lne_lt0 x : (lne x < 0) = (x < 1).
+Proof. by rewrite 2!ltNge lne_ge0. Qed.
+
+Lemma lne_eq0 x : (lne x == 0) = (x == 1).
+Proof.
+apply/idP/idP => /eqP; last by move=> ->; rewrite lne1.
+have [|x0] := leP x 0.
+  by case: x => [r| |]//; rewrite lee_fin => /= ->.
+rewrite -lne1 => /lne_inj.
+rewrite ?in_itv/= ?leey ?andbT// => /(_ _ _)/eqP.
+by apply => //; exact: ltW.
+Qed.
+
+Lemma lne_gt0 x : (0 < lne x) = (1 < x).
+Proof. by rewrite 2!lt_neqAle eq_sym lne_eq0 eq_sym lne_ge0. Qed.
+
+Lemma lne_le0 x : (lne x <= 0) = (x <= 1).
+Proof. by rewrite 2!leNgt lne_gt0. Qed.
+
+End Lne.
+
 Section poweR.
 Local Open Scope ereal_scope.
 Context {R : realType}.
@@ -1332,7 +1473,7 @@ move=> /andP[a0 a1].
 have : forall n, harmonic n <= riemannR a n.
   move=> [/=|n]; first by rewrite powR1 invr1.
   rewrite -[leRHS]div1r ler_pdivlMr ?powR_gt0// mulrC ler_pdivrMr//.
-  by rewrite mul1r -[leRHS]powRr1// (ler_powR)// ler1n.
+  by rewrite mul1r -[leRHS]powRr1// ler_powR// ler1n.
 move/(series_le_cvg harmonic_ge0 (fun i => ltW (riemannR_gt0 i a0))).
 by move/contra_not; apply; exact: dvg_harmonic.
 Qed.
diff --git a/theories/ftc.v b/theories/ftc.v
index 89676f684a..95bb5fe753 100644
--- a/theories/ftc.v
+++ b/theories/ftc.v
@@ -1430,7 +1430,7 @@ Lemma ge0_integration_by_substitutionNy G a :
   \int[mu]_(x in `[a, +oo[) ((G \o -%R) x)%:E.
 Proof.
 move=> /continuous_within_itvNycP[cG GNa] G0.
-have Dopp : (@GRing.opp R)^`() = cst (-1).
+have Dopp : (@GRing.opp R)^`() = cst (- 1)%R.
   by apply/funext => z; rewrite derive1E derive_val.
 rewrite decreasing_ge0_integration_by_substitutiony//; last 7 first.
   by move=> x y _ _; rewrite ltrN2.
diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index 9808470294..71c4818427 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -151,10 +151,10 @@ Proof.
 move=> mD r; rewrite /Rintegral/= integral_cst//.
 have := leey (mu D); rewrite le_eqVlt => /predU1P[->/=|muy]; last first.
   by rewrite fineM// ge0_fin_numE.
-rewrite mulr_infty/=; have [_|r0|r0] := sgrP r.
-- by rewrite mul0e/= mulr0.
-- by rewrite mul1e/= mulr0.
-- by rewrite mulN1e/= mulr0.
+rewrite mulr0 mulr_infty/=; have [_|r0|r0] := sgrP r.
+- by rewrite mul0e.
+- by rewrite mul1e.
+- by rewrite mulN1e.
 Qed.
 
 Lemma le_Rintegral D f1 f2 : measurable D ->
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
index 399ca49b3a..6af95b7d03 100644
--- a/theories/normedtype_theory/normed_module.v
+++ b/theories/normedtype_theory/normed_module.v
@@ -952,16 +952,16 @@ move=> [:apoo] [:bnoo] [:poopoo] [:poonoo]; move: a b => [a| |] [b| |] //.
   exact: cvgM.
 - move: f g a; abstract: apoo.
   move=> {}f {}g {}a + fa goo; have [a0 _|a0 _|->] := ltgtP a 0%R.
-  + rewrite mulry ltr0_sg// ?mulN1e.
+  + rewrite mulry ltr0_sg// mulN1e.
     by under eq_fun do rewrite muleC; exact: (cvgeM_lt0_pinfty a0).
-  + rewrite mulry gtr0_sg// ?mul1e.
+  + rewrite mulry gtr0_sg// mul1e.
     by under eq_fun do rewrite muleC; exact: (cvgeM_gt0_pinfty a0).
   + by rewrite /mule_def eqxx.
 - move: f g a; abstract: bnoo.
   move=> {}f {}g {}a + fa goo; have [a0 _|a0 _|->] := ltgtP a 0%R.
-  + rewrite mulrNy ltr0_sg// ?mulN1e.
+  + rewrite mulrNy ltr0_sg// mulN1e.
     by under eq_fun do rewrite muleC; exact: (cvgeM_lt0_ninfty a0).
-  + rewrite mulrNy gtr0_sg// ?mul1e.
+  + rewrite mulrNy gtr0_sg// mul1e.
     by under eq_fun do rewrite muleC; exact: (cvgeM_gt0_ninfty a0).
   + by rewrite /mule_def eqxx.
 - rewrite mule_defC => ? foo gb; rewrite muleC.