diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b6..0afa4cb332 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,12 +4,21 @@
 
 ### Added
 
+- in `ereal_normedtype.v`:
+  + lemma `ge0_cvgMly`
+
 ### Changed
 
+- in `lebesgue_integral_nonneg.v`, generalized and deprecated:
+  + lemma `ge0_integralZl_EFin` (no condition on `k`)
+
 ### Renamed
 
 ### Generalized
 
+- in `lebesgue_integral_nonneg.v`:
+  + lemmas `ge0_integralZl`, `ge0_integralZr`
+
 ### Deprecated
 
 ### Removed
diff --git a/theories/hoelder.v b/theories/hoelder.v
index 15861f1eed..44fce50f98 100644
--- a/theories/hoelder.v
+++ b/theories/hoelder.v
@@ -448,8 +448,7 @@ rewrite [leLHS](_ : _ = 'N_1[(F \* G)%R] * 'N_p%:E[f] * 'N_q%:E[g]).
     rewrite ger0_norm; first by rewrite mulr_ge0 ?divr_ge0 ?fine_ge0 ?Lnorm_ge0.
     by rewrite mulrACA -normrM EFinM; over.
   rewrite ge0_integralZr//.
-    - by do 2 apply: measurableT_comp => //; exact: measurable_funM.
-    - by rewrite lee_fin mulr_ge0// invr_ge0 fine_ge0// Lnorm_ge0.
+    by do 2 apply: measurableT_comp => //; exact: measurable_funM.
   rewrite -!muleA [X in _ * X](_ : _ = 1) ?mule1// EFinM muleACA.
   rewrite (_ : _ * 'N_p%:E[f] = 1) ?mul1e.
     rewrite -[X in _ * X]fineK; first by rewrite ge0_fin_numE ?ltey// Lnorm_ge0.
@@ -477,16 +476,14 @@ rewrite ge0_integralD//.
   by apply: measurableT_comp_powR => //; exact: measurable_normalized.
 under eq_integral do rewrite EFinM.
 rewrite [X in X + _]ge0_integralZr//.
+- by move=> x _; rewrite lee_fin powR_ge0.
 - apply: measurableT_comp => //.
   by apply: measurableT_comp_powR => //; exact: measurable_normalized.
-- by move=> x _; rewrite lee_fin powR_ge0.
-- by rewrite lee_fin invr_ge0 ltW.
 under [X in _ + X]eq_integral => x _ do rewrite EFinM.
 rewrite ge0_integralZr//.
+- by move=> x _; rewrite lee_fin powR_ge0.
 - apply: measurableT_comp => //.
   by apply: measurableT_comp_powR => //; exact: measurable_normalized.
-- by move=> x _; rewrite lee_fin powR_ge0.
-- by rewrite lee_fin invr_ge0 ltW.
 rewrite integral_normalized//; first exact: integrable_powR.
 rewrite integral_normalized//; first exact: integrable_powR.
 by rewrite 2!mul1e -EFinD pq.
@@ -641,7 +638,7 @@ apply: (@le_lt_trans _ _ x).
       exact/measurableT_comp_powR/measurableT_comp.
   - by move=> ? _; rewrite lee_fin.
 rewrite {}/x; under eq_integral do rewrite EFinM.
-rewrite ge0_integralZl_EFin ?powR_ge0//.
+rewrite ge0_integralZl ?powR_ge0//.
   by apply/measurable_EFinP/measurable_funD => //;
     exact/measurableT_comp_powR/measurableT_comp.
 rewrite lte_mul_pinfty ?lee_fin ?powR_ge0//.
diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
index 165e976a6b..1762e6b2d2 100644
--- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v
@@ -268,14 +268,13 @@ by rewrite mul0e.
 Qed.
 
 #[local] Lemma integral_measure_of_densityMindic (r : R) (A : set T) : measurable A ->
-  (0 <= r)%R ->
   \int[mu]_x (r%:E * (\1_A x)%:E * (h x)%:E) = r%:E * mu' A.
 Proof.
-move=> mA r0.
+move=> mA.
 under eq_integral do rewrite -muleA.
 rewrite ge0_integralZl//=.
-- apply: emeasurable_funM => //; by apply /measurable_EFinP.
 - by move=> x _; apply: mule_ge0; rewrite ?lee_fin.
+- apply: emeasurable_funM => //; by apply /measurable_EFinP.
 - by rewrite integral_measure_of_density_indic.
 Qed.
 
diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v
index 9a50cc5a78..b69f976f28 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integrable.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v
@@ -32,10 +32,10 @@ From mathcomp Require Import lebesgue_integral_nonneg.
 
 Reserved Notation "mu .-integrable" (at level 2, format "mu .-integrable").
 
-Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
+
 Import Order.TTheory GRing.Theory Num.Def Num.Theory.
 Import numFieldNormedType.Exports.
 
@@ -522,9 +522,9 @@ End integrable_ae.
 
 Section integralZl.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
-Variable (f : T -> \bar R).
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
+  (f : T -> \bar R).
 Hypothesis intf : mu.-integrable D f.
 
 Let mesf : measurable_fun D f. Proof. exact: measurable_int intf. Qed.
@@ -534,13 +534,13 @@ Lemma integralZl r :
 Proof.
 have /orP[r0|r0] := le_total r 0%R.
 - rewrite [in LHS]integralE// le0_funeposM// le0_funenegM//.
-  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funeneg _)) ?oppr_ge0//.
-  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funepos _)) ?oppr_ge0//.
-  rewrite !EFinN addeC !mulNe oppeK -muleBr ?integrable_add_def//.
-  by rewrite [in RHS]integralE.
+  rewrite (ge0_integralZl _ _ _ (measurable_funeneg _))//.
+  rewrite (ge0_integralZl _ _ _ (measurable_funepos _))//.
+  rewrite !mulNe oppeK addeC -muleBr ?integrable_add_def//.
+  by rewrite -integralE.
 - rewrite [in LHS]integralE// ge0_funeposM// ge0_funenegM//=.
-  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funepos _) r0)//.
-  rewrite (ge0_integralZl_EFin _ _ _ (measurable_funeneg _) r0)//.
+  rewrite (ge0_integralZl _ _ _ (measurable_funepos _))//.
+  rewrite (ge0_integralZl _ _ _ (measurable_funeneg _))//.
   by rewrite -muleBr 1?[in RHS]integralE// integrable_add_def.
 Qed.
 
@@ -552,9 +552,9 @@ End integralZl.
 
 Section integralD_EFin.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
-Variables f1 f2 : T -> R.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
+  (f1 f2 : T -> R).
 Let g1 := EFin \o f1.
 Let g2 := EFin \o f2.
 Hypothesis if1 : mu.-integrable D g1.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
index 9f05a24ac3..a315c46359 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
@@ -36,7 +36,6 @@ From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable.
 (*                                                                            *)
 (******************************************************************************)
 
-Unset SsrOldRewriteGoalsOrder.  (* remove the line when requiring MathComp >= 2.6 *)
 Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
@@ -306,7 +305,7 @@ move=> mA1 mA2 /=; rewrite /product_measure1 /=.
 rewrite (eq_integral (fun x => (\1_A1 x)%:E * m2 A2)).
   by move=> x _; rewrite indicE; have [xA1|xA1] /= := boolP (x \in A1);
     [rewrite in_xsectionX// mul1e|rewrite mul0e notin_xsectionX].
-rewrite ge0_integralZr ?integral_indic ?setIT//; exact: measurableT_comp.
+by rewrite ge0_integralZr ?integral_indic ?setIT//; exact: measurableT_comp.
 Qed.
 
 End product_measure1E.
@@ -461,7 +460,7 @@ Proof.
 have mA1A2 : measurable (A1 `*` A2) by apply: measurableX.
 transitivity (\int[m2]_y (m1 \o ysection (A1 `*` A2)) y) => //.
 rewrite (_ : _ \o _ = fun y => m1 A1 * (\1_A2 y)%:E); last first.
-  rewrite ge0_integralZl ?integral_indic ?setIT//; exact: measurableT_comp.
+  by rewrite ge0_integralZl ?integral_indic ?setIT//; exact: measurableT_comp.
 rewrite funeqE => y; rewrite indicE.
 have [yA2|yA2] := boolP (y \in A2); first by rewrite mule1 /= in_ysectionX.
 by rewrite mule0 /= notin_ysectionX.
@@ -588,9 +587,8 @@ rewrite ge0_integral_fsum //.
 - by move=> r y _; rewrite EFinM nnfun_muleindic_ge0.
 apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}].
 under eq_fun do rewrite EFinM.
-rewrite ge0_integralZl//; [|by rewrite lee_fin|].
-- exact/measurable_EFinP/measurableT_comp.
-- by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE.
+rewrite ge0_integralZl//; first exact/measurable_EFinP/measurableT_comp.
+by rewrite -/((m2 \o xsection _) x) -indic_fubini_tonelli_FE.
 Qed.
 
 Lemma sfun_measurable_fun_fubini_tonelli_F : measurable_fun [set: T1] F.
@@ -610,9 +608,8 @@ rewrite ge0_integral_fsum //.
 - by move=> r x _; rewrite EFinM nnfun_muleindic_ge0.
 apply: eq_fsbigr => i; rewrite inE => -[/= t _ <-{i}].
 under eq_fun do rewrite EFinM.
-rewrite ge0_integralZl//; [|by rewrite lee_fin|].
-- exact/measurable_EFinP/measurableT_comp.
-- by rewrite -/((m1 \o ysection _) y) -indic_fubini_tonelli_GE.
+rewrite ge0_integralZl//; first exact/measurable_EFinP/measurableT_comp.
+by rewrite -/((m1 \o ysection _) y) -indic_fubini_tonelli_GE.
 Qed.
 
 Lemma sfun_measurable_fun_fubini_tonelli_G : measurable_fun setT G.
@@ -634,16 +631,14 @@ under [LHS]eq_integral
 transitivity (\sum_(k \in range f)
   \int[m1]_x (k%:E * fubini_F m2 (EFin \o \1_(f @^-1` [set k])) x)).
   apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}].
-  rewrite ge0_integralZl//.
-  - exact/measurable_EFinP.
-  - by rewrite lee_fin.
-  rewrite indic_fubini_tonelli1// -ge0_integralZl//; last by rewrite lee_fin.
-  - exact: indic_measurable_fun_fubini_tonelli_F.
-  - by move=> /= x _; exact: indic_fubini_tonelli_F_ge0.
+  rewrite ge0_integralZl//=; first exact/measurable_EFinP.
+  rewrite indic_fubini_tonelli1// -ge0_integralZl//.
+    by move=> /= x _; exact: indic_fubini_tonelli_F_ge0.
+  exact: indic_measurable_fun_fubini_tonelli_F.
 rewrite -ge0_integral_fsum; [by []| | |by []|]; first 2 last.
 - apply: eq_integral => x _; rewrite sfun_fubini_tonelli_FE.
   by under eq_fsbigr do rewrite indic_fubini_tonelli_FE//.
-- by move=> r; apply/measurable_funeM/indic_measurable_fun_fubini_tonelli_F.
+- by move=> r; exact/measurable_funeM/indic_measurable_fun_fubini_tonelli_F.
 move=> r x _; rewrite /fubini_F.
 have [r0|r0] := leP 0%R r.
   by rewrite mule_ge0//; exact: indic_fubini_tonelli_F_ge0.
@@ -660,12 +655,10 @@ under [LHS]eq_integral
 transitivity (\sum_(k \in range f)
   \int[m2]_x (k%:E * (fubini_G m1 (EFin \o \1_(f @^-1` [set k])) x))).
   apply: eq_fsbigr => i; rewrite inE => -[z _ <-{i}].
-  rewrite ge0_integralZl//.
-  - exact/measurable_EFinP.
-  - by rewrite lee_fin.
-  rewrite indic_fubini_tonelli2// -ge0_integralZl//; last by rewrite lee_fin.
-  - exact: indic_measurable_fun_fubini_tonelli_G.
-  - by move=> /= x _; exact: indic_fubini_tonelli_G_ge0.
+  rewrite ge0_integralZl//=; first exact/measurable_EFinP.
+  rewrite indic_fubini_tonelli2// -ge0_integralZl//.
+    by move=> /= x _; exact: indic_fubini_tonelli_G_ge0.
+  exact: indic_measurable_fun_fubini_tonelli_G.
 rewrite -ge0_integral_fsum; [by []| | |by []|]; first 2 last.
 - apply: eq_integral => x _; rewrite sfun_fubini_tonelli_GE.
   by under eq_fsbigr do rewrite indic_fubini_tonelli_GE//.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
index 19eb8049c1..a4af3f425b 100644
--- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
+++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
@@ -110,26 +110,26 @@ rewrite integral_mkcond integral0_eq// => x _.
 by rewrite /restrict; case: ifPn => //; rewrite in_set0.
 Qed.
 
-Section ge0_integralZl_EFin.
+Section ge0_integralZ.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
-Variables f1 f2 : T -> \bar R.
-Hypothesis f10 : forall x, D x -> 0 <= f1 x.
-Hypothesis mf1 : measurable_fun D f1.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
+  (f : T -> \bar R).
+Hypothesis f0 : forall x, D x -> 0 <= f x.
+Hypothesis mf : measurable_fun D f.
 
 Import HBNNSimple.
 
-Lemma ge0_integralZl_EFin k : (0 <= k)%R ->
-  \int[mu]_(x in D) (k%:E * f1 x) = k%:E * \int[mu]_(x in D) f1 x.
+Let ge0_integralZl_EFin_subproof k : (0 <= k)%R ->
+  \int[mu]_(x in D) (k%:E * f x) = k%:E * \int[mu]_(x in D) f x.
 Proof.
 rewrite integral_mkcond erestrict_scale [in RHS]integral_mkcond => k0.
-set h1 := f1 \_ D.
-have h10 x : 0 <= h1 x by apply: erestrict_ge0.
-have mh1 : measurable_fun setT h1 by exact/(measurable_restrictT _ _).1.
-pose g := nnsfun_approx measurableT mh1.
+set h := f \_ D.
+have h0 x : 0 <= h x by apply: erestrict_ge0.
+have mh : measurable_fun setT h by exact/(measurable_restrictT _ _).1.
+pose g := nnsfun_approx measurableT mh.
 pose kg := fun n => scale_nnsfun (g n) k0.
-rewrite (@nd_ge0_integral_lim _ _ _ mu (fun x => k%:E * h1 x) kg).
+rewrite (@nd_ge0_integral_lim _ _ _ mu (fun x => k%:E * h x) kg).
 - by move=> t; rewrite mule_ge0.
 - by move=> x m n mn; rewrite /kg ler_pM//; exact/lefP/nd_nnsfun_approx.
 - move=> x.
@@ -140,17 +140,64 @@ rewrite (_ : (fun _ => _) = (fun n => k%:E * sintegral mu (g n))).
   by under eq_fun do rewrite (sintegralrM mu k (g _)).
 rewrite limeMl //.
   by apply: is_cvg_sintegral => // x m n mn; exact/lefP/nd_nnsfun_approx.
-by rewrite -(nd_ge0_integral_lim mu h10)// => [x m n mn|x];
+by rewrite -(nd_ge0_integral_lim mu h0)// => [x m n mn|x];
   [exact/lefP/nd_nnsfun_approx|exact: cvg_nnsfun_approx].
 Qed.
 
-End ge0_integralZl_EFin.
+#[deprecated(since="mathcomp-analysis 1.20.0", note="consider using `ge0_integralZl`")]
+Lemma ge0_integralZl_EFin k :
+  \int[mu]_(x in D) (k%:E * f x) = k%:E * \int[mu]_(x in D) f x.
+Proof.
+have [k0|k0] := leP 0%R k; first exact: ge0_integralZl_EFin_subproof.
+rewrite integralE [X in X - _](_ : _ = 0).
+  rewrite (eq_integral (cst 0)) ?integral0// => x Dx.
+  by rewrite (le0_funeposM _ (ltW k0)) (@ge0_funenegE _ _ D)//= mule0.
+rewrite (eq_integral (fun x => (- k)%:E * f x)).
+  move=> x Dx.
+  by rewrite (le0_funenegM _ (ltW k0)) (@ge0_funeposE _ _ D).
+rewrite ge0_integralZl_EFin_subproof ?oppr_ge0 ?ltW//.
+by rewrite sub0e EFinN mulNe oppeK.
+Qed.
+
+Let ge0_integralZly :
+  \int[mu]_(x in D) (+oo * f x) = +oo * \int[mu]_(x in D) f x.
+Proof.
+rewrite (eq_integral (fun x => limn (fun n => n%:R%:E * f x))).
+  by move=> x /[!inE] Dx; apply/esym/cvg_lim => //; exact/ ge0_cvgeMly/f0.
+rewrite monotone_convergence//.
+- by move=> n; exact: emeasurable_funM.
+- by move=> n x Dx; rewrite mule_ge0 ?f0.
+- by move=> x Dx n m nm; rewrite lee_wpmul2r ?f0// lee_fin ler_nat.
+- #[warning="-deprecated"]under eq_fun do rewrite ge0_integralZl_EFin//.
+  by apply/cvg_lim => //; exact/ge0_cvgeMly/integral_ge0.
+Qed.
+
+Lemma ge0_integralZl k : \int[mu]_(x in D) (k * f x) = k * \int[mu]_(x in D) f x.
+Proof.
+#[warning="-deprecated"]move: k => [r| |]; [exact: ge0_integralZl_EFin|exact: ge0_integralZly|].
+rewrite integralE [X in X - _](_ : _ = 0).
+  rewrite (eq_integral (cst 0)) ?integral0// => x /set_mem Dx.
+  by rewrite funeposE/=; apply/max_idPr; rewrite mule_le0_ge0// f0.
+rewrite (eq_integral (fun x => +oo * f x)).
+  move=> x /set_mem Dx; rewrite funenegE/= -mulNe/= max_l//.
+  by rewrite mule_ge0 ?f0.
+by rewrite ge0_integralZly// sub0e -mulNe.
+Qed.
+
+Lemma ge0_integralZr k :
+  \int[mu]_(x in D) f x * k = (\int[mu]_(x in D) f x) * k.
+Proof.
+under eq_integral do rewrite muleC.
+by rewrite ge0_integralZl// muleC.
+Qed.
+
+End ge0_integralZ.
 
 Section ge0_linearityD.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variable mu : {measure set T -> \bar R}.
-Variables (D : set T) (mD : measurable D) (f1 f2 : T -> \bar R).
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
+  (f1 f2 : T -> \bar R).
 Hypothesis f10 : forall x, D x -> 0 <= f1 x.
 Hypothesis mf1 : measurable_fun D f1.
 Hypothesis f20 : forall x, D x -> 0 <= f2 x.
@@ -195,9 +242,9 @@ End ge0_linearityD.
 
 Section ge0_integral_sum.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
-Variables (I : Type) (f : I -> (T -> \bar R)).
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
+  {I : Type} (f : I -> (T -> \bar R)).
 Hypothesis mf : forall n, measurable_fun D (f n).
 Hypothesis f0 : forall n x, D x -> 0 <= f n x.
 
@@ -218,9 +265,9 @@ End ge0_integral_sum.
 
 Section ge0_integral_fsum.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
-Variables (I : choiceType) (f : I -> (T -> \bar R)).
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
+  {I : choiceType} (f : I -> (T -> \bar R)).
 Hypothesis mf : forall n, measurable_fun D (f n).
 Hypothesis f0 : forall n x, D x -> 0 <= f n x.
 
@@ -236,9 +283,9 @@ End ge0_integral_fsum.
 
 Section integral_nneseries.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D).
-Variable f : (T -> \bar R)^nat.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D)
+  (f : (T -> \bar R)^nat).
 Hypothesis mf : forall n, measurable_fun D (f n).
 Hypothesis f0 : forall n x, D x -> 0 <= f n x.
 
@@ -254,76 +301,6 @@ Qed.
 
 End integral_nneseries.
 
-(**md Generalization of `ge0_integralZl_EFin` to a constant potentially $+\infty$
-   using the monotone convergence theorem: *)
-Section ge0_integralZ.
-Local Open Scope ereal_scope.
-Context d {T : measurableType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
-Variables (D : set T) (mD : measurable D) (f : T -> \bar R).
-Hypothesis mf : measurable_fun D f.
-Implicit Type k : \bar R.
-
-Lemma ge0_integralZl k : (forall x, D x -> 0 <= f x) ->
-  0 <= k -> \int[mu]_(x in D) (k * f x) = k * \int[mu]_(x in D) (f x).
-Proof.
-move=> f0; move: k => [k|_|//]; first exact: ge0_integralZl_EFin.
-pose g : (T -> \bar R)^nat := fun n x => n%:R%:E * f x.
-have mg n : measurable_fun D (g n) by apply: measurable_funeM.
-have g0 n x : D x -> 0 <= g n x.
-  by move=> Dx; apply: mule_ge0; [rewrite lee_fin|exact:f0].
-have nd_g x : D x -> nondecreasing_seq (g ^~ x).
-  by move=> Dx m n mn; rewrite lee_wpmul2r ?f0// lee_fin ler_nat.
-pose h := fun x => limn (g^~ x).
-transitivity (\int[mu]_(x in D) limn (g^~ x)).
-  apply: eq_integral => x Dx; apply/esym/cvg_lim => //.
-  have [fx0|fx0|fx0] := ltgtP 0 (f x).
-  - rewrite gt0_mulye//; apply/cvgeyPgey; near=> M.
-    have M0 : (0 <= M)%R by [].
-    rewrite /g; case: (f x) fx0 => [r r0|_|//]; last first.
-      by exists 1%N => // m /= m0; rewrite mulry gtr0_sg// ?ltr0n// mul1e leey.
-    near=> n; rewrite lee_fin -ler_pdivrMr//.
-    near: n; exists (truncn (M / r)).+1 => // m /= Mrm.
-    by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat.
-  - rewrite lt0_mulye//; apply/cvgeNyPleNy; near=> M;
-    have M0 : (M <= 0)%R by [].
-    rewrite /g; case: (f x) fx0 => [r r0|//|_]; last first.
-      by exists 1%N => // m /= m0; rewrite mulrNy gtr0_sg// ?ltr0n// mul1e leNye.
-    near=> n; rewrite lee_fin -ler_ndivrMr//.
-    near: n; exists (truncn (M / r)).+1 => // m /= Mrm.
-    by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat.
-  - rewrite -fx0 mule0 /g -fx0.
-    rewrite [X in X @ _](_ : _ = cst 0)//.
-    by under eq_fun do rewrite mule0.
-rewrite (monotone_convergence mu mD mg g0 nd_g).
-under eq_fun do rewrite /g ge0_integralZl_EFin//.
-have : 0 <= \int[mu]_(x in D) f x by exact: integral_ge0.
-rewrite le_eqVlt => /predU1P[<-|if_gt0].
-  by rewrite mule0; under eq_fun do rewrite mule0; rewrite lim_cst.
-rewrite gt0_mulye//; apply/cvg_lim => //; apply/cvgeyPgey; near=> M.
-have M0 : (0 <= M)%R by [].
-near=> n; have [ifoo|] := ltP (\int[mu]_(x in D) f x) +oo; last first.
-  rewrite leye_eq => /eqP ->; rewrite mulry muleC gt0_mulye ?leey//.
-  by near: n; exists 1%N => // n /= n0; rewrite gtr0_sg// ?lte_fin// ltr0n.
-rewrite -(@fineK _ (\int[mu]_(x in D) f x)).
-  by rewrite fin_numElt ifoo (le_lt_trans _ if_gt0).
-rewrite -lee_pdivrMr//.
-  by move: if_gt0 ifoo; case: (\int[mu]_(x in D) f x).
-near: n.
-exists (truncn (M * (fine (\int[mu]_(x in D) f x))^-1)).+1 => //.
-move=> n /=; rewrite -(@ler_nat R) -lee_fin; apply: le_trans.
-by rewrite lee_fin ltW// truncnS_gt.
-Unshelve. all: by end_near. Qed.
-
-Lemma ge0_integralZr k : (forall x, D x -> 0 <= f x) ->
-  0 <= k -> \int[mu]_(x in D) f x * k = (\int[mu]_(x in D) f x) * k.
-Proof.
-move=> f0 k0; under eq_integral do rewrite muleC.
-by rewrite ge0_integralZl// muleC.
-Qed.
-
-End ge0_integralZ.
-
 Section integralZl_indic.
 Local Open Scope ereal_scope.
 Context {d} {T : measurableType d} {R : realType}
@@ -338,7 +315,7 @@ move=> fk0 mfk; have [k0|k0] := ltP k 0%R.
   rewrite integral0_eq//; first by move=> x _; rewrite fk0// indic0 mulr0.
   by rewrite integral0_eq ?mule0// => x _; rewrite fk0// indic0.
 under eq_integral do rewrite EFinM.
-rewrite ge0_integralZl//; exact/measurable_EFinP.
+by rewrite ge0_integralZl//; exact/measurable_EFinP.
 Qed.
 
 Import HBNNSimple.
@@ -377,8 +354,8 @@ rewrite [LHS]ge0_integral_fsum//.
   - by move=> r; exact/measurable_EFinP/measurableT_comp.
   - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0.
 rewrite -[RHS]ge0_integralZl//.
-  - by apply: measurableT_comp => //; exact: measurable_funTS.
   - by move=> x _; rewrite lee_fin.
+  - by apply: measurableT_comp => //; exact: measurable_funTS.
 under [RHS]eq_integral.
   move=> x xD; rewrite fimfunE -fsumEFin// ge0_mule_fsumr.
     by move=> r; rewrite EFinM nnfun_muleindic_ge0.
@@ -387,8 +364,8 @@ rewrite [RHS]ge0_integral_fsum//.
   - by move=> r; apply/measurable_EFinP; do 2 apply/measurableT_comp => //.
   - by move=> n x _; rewrite EFinM mule_ge0// nnfun_muleindic_ge0.
 apply: eq_fsbigr => r _; rewrite ge0_integralZl//.
-- exact/measurable_EFinP/measurableT_comp.
 - by move=> t _; rewrite nnfun_muleindic_ge0.
+- exact/measurable_EFinP/measurableT_comp.
 - by rewrite !integralZl_indic_nnsfun//= integral_mscale_indic// muleCA.
 Qed.
 
@@ -456,9 +433,9 @@ End integralN.
 
 Section integral_cst.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType)
-        (mu : {measure set T -> \bar R}).
-Variables (f : T -> \bar R) (D : set T) (mD : measurable D).
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}) (f : T -> \bar R) (D : set T)
+  (mD : measurable D).
 
 Lemma sintegral_EFin_cst (x : {nonneg R}) :
   sintegral mu (cst x%:num \_ D) = x%:num%:E * mu D.
@@ -730,8 +707,8 @@ End integral_measure_add_nnsfun.
 
 Section integral_mfun_measure_sum.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variable m_ : {measure set T -> \bar R}^nat.
+Context {d} {T : measurableType d} {R : realType}
+  (m_ : {measure set T -> \bar R}^nat).
 
 Import HBNNSimple.
 
@@ -827,8 +804,8 @@ End integral_measure_series.
 
 Section ge0_integral_measure_series.
 Local Open Scope ereal_scope.
-Context d (T : measurableType d) (R : realType).
-Variable m_ : {measure set T -> \bar R}^nat.
+Context {d} {T : measurableType d} {R : realType}
+  (m_ : {measure set T -> \bar R}^nat).
 Let m := mseries m_ O.
 
 Import HBNNSimple.
@@ -1091,8 +1068,8 @@ End integral_patch.
 Section ge0_cvgn_integral.
 Local Open Scope ereal_scope.
 Import MeasurableR.
-Context {R : realType} (mu : {measure set (@measurableTypeR R) -> \bar R}).
-Variable f : R -> R.
+Context {R : realType} (mu : {measure set (@measurableTypeR R) -> \bar R})
+ (f : R -> R).
 Hypothesis f0 : (forall x, 0 <= f x)%R.
 
 
@@ -1200,7 +1177,7 @@ move=> mD mf; rewrite fin_num_abs; case H : LHS; apply/esym.
 Qed.
 
 Section ae_measurable_fun.
-Context d (T : measurableType d) (R : realType)
+Context {d} {T : measurableType d} {R : realType}
         (mu : {measure set T -> \bar R}).
 Hypothesis cmu : measure_is_complete mu.
 Variables (D : set T) (f g : T -> \bar R).
@@ -1232,7 +1209,7 @@ End ae_measurable_fun.
 
 Section ge0_integral_counting.
 Local Open Scope ereal_scope.
-Variable R : realType.
+Context {R : realType}.
 
 Lemma counting_dirac (A : set nat) :
   counting A = \sum_(n <oo) \d_ n A :> \bar R.
@@ -1433,9 +1410,9 @@ Arguments ae_eq_integral {d T R mu D} g.
 
 Section ae_ge0_le_integral.
 Local Open Scope ereal_scope.
-Context d {T : measurableType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
-Variables (D : set T) (mD : measurable D) (f1 f2 : T -> \bar R).
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R})
+  (D : set T) (mD : measurable D) (f1 f2 : T -> \bar R).
 Hypothesis f10 : forall x, D x -> 0 <= f1 x.
 Hypothesis mf1 : measurable_fun D f1.
 Hypothesis f20 : forall x, D x -> 0 <= f2 x.
@@ -1493,8 +1470,8 @@ Qed.
 Local Close Scope ereal_scope.
 
 Section integral_bounded.
-Context d {T : measurableType d} {R : realType}.
-Variable mu : {measure set T -> \bar R}.
+Context {d} {T : measurableType d} {R : realType}
+  (mu : {measure set T -> \bar R}).
 Local Open Scope ereal_scope.
 
 Lemma integral_le_bound (D : set T) (f : T -> \bar R) (M : \bar R) :
@@ -1669,8 +1646,8 @@ Qed.
 End ge0_nondecreasing_set_cvg_integral.
 
 Section le0_nondecreasing_set_cvg_integral.
-Context {d : measure_display} {T : measurableType d} {R : realType}.
-Variables (F : (set T)^nat) (f : T -> \bar R) (mu : measure T R).
+Context {d : measure_display} {T : measurableType d} {R : realType}
+  (F : (set T)^nat) (f : T -> \bar R) (mu : measure T R).
 Local Open Scope ereal_scope.
 Hypotheses (nndF : nondecreasing_seq F) (mF : forall i, measurable (F i)).
 Hypothesis mf : forall i, measurable_fun (F i) f.
diff --git a/theories/lebesgue_integral_theory/radon_nikodym.v b/theories/lebesgue_integral_theory/radon_nikodym.v
index f5c1bda84d..1f6b1d3239 100644
--- a/theories/lebesgue_integral_theory/radon_nikodym.v
+++ b/theories/lebesgue_integral_theory/radon_nikodym.v
@@ -894,10 +894,9 @@ under [RHS]eq_integral do rewrite EFinM.
 rewrite integralZl_indic_nnsfun => //.
 under eq_integral do rewrite EFinM -muleA.
 rewrite ge0_integralZl//.
+- by move=> t Et; rewrite mule_ge0 ?lee_fin ?f_ge0.
 - apply: emeasurable_funM; first exact/measurable_EFinP.
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
-- by move=> t Et; rewrite mule_ge0 ?lee_fin ?f_ge0.
-- by move: rhn; rewrite inE => -[t _ <-]; rewrite lee_fin.
 under eq_integral do rewrite muleC.
 rewrite (eq_integral (g \_ (h n @^-1` [set r]))).
   by move=> x xE; rewrite epatch_indic.
diff --git a/theories/normedtype_theory/ereal_normedtype.v b/theories/normedtype_theory/ereal_normedtype.v
index 105cc2e833..f49f48983c 100644
--- a/theories/normedtype_theory/ereal_normedtype.v
+++ b/theories/normedtype_theory/ereal_normedtype.v
@@ -69,7 +69,7 @@ Proof. by rewrite /limf_einf; under eq_fun do rewrite oppeK. Qed.
 End limf_esup_einf.
 
 Section limf_esup_einf_realType.
-Variables (T : choiceType) (X : filteredType T) (R : realType).
+Context {T : choiceType} {X : filteredType T} {R : realType}.
 Implicit Types (f : X -> \bar R) (F : set_system X).
 Local Open Scope ereal_scope.
 
@@ -270,11 +270,25 @@ Proof. by rewrite cvgeNyPlt. Qed.
 
 End ecvg_infty_realField.
 
+Local Open Scope ereal_scope.
+Lemma ge0_cvgeMly (R : realType) (a : \bar R) : 0 <= a ->
+  (n%:R%:E * a) @[n --> \oo] --> +oo * a.
+Proof.
+rewrite le_eqVlt => /predU1P[<-|a_gt0].
+  by rewrite mule0; under eq_fun do rewrite mule0; exact: cvg_cst.
+rewrite gt0_mulye//; apply/cvgeyPge => A.
+move: a a_gt0 => [r /[!(@lte_fin R)] r0|_ |//].
+- near=> n; rewrite -EFinM lee_fin -ler_pdivrMr//.
+  by near: n; exact: nbhs_infty_ger.
+- near=> n; rewrite gt0_muley ?leey// lte_fin ltr0n//.
+  by near: n; exact: nbhs_infty_gt.
+Unshelve. all: by end_near. Qed.
+Local Close Scope ereal_scope.
+
 Section open_closed_sets_ereal.
-Variable R : realFieldType (* TODO: generalize to numFieldType? *).
+Context {R : realFieldType} (* TODO: generalize to numFieldType? *).
 Local Open Scope ereal_scope.
-Implicit Types x y : \bar R.
-Implicit Types r : R.
+Implicit Types (x y : \bar R) (r : R).
 
 Lemma open_ereal_lt y : open [set r : R | r%:E < y].
 Proof.
@@ -360,7 +374,7 @@ Qed.
 End open_closed_sets_ereal.
 
 Section ereal_is_hausdorff.
-Variable R : realFieldType.
+Context {R : realFieldType}.
 Implicit Types r : R.
 
 Lemma nbhs_image_EFin r (X : set R) :
@@ -456,7 +470,7 @@ Proof. exact: cvge_to_le. Qed.
 End ProperFilterERealType.
 
 Lemma cvgenyP {R : realType} {T} {F : set_system T} {FF : Filter F} (f : T -> nat) :
-   (((f n)%:R : R)%:E @[n --> F] --> +oo%E) <-> (f @ F --> \oo).
+  (((f n)%:R : R)%:E @[n --> F] --> +oo%E) <-> (f @ F --> \oo).
 Proof. by rewrite cvgeryP cvgrnyP. Qed.
 
 Section nbhs_ereal.
@@ -479,7 +493,7 @@ Qed.
 End nbhs_ereal.
 
 Section ereal_OrderNbhs.
-Variable R : realFieldType.
+Context {R : realFieldType}.
 
 Let ereal_order_nbhsE (x : \bar R) :
   nbhs x = filter_from (fun i => itv_open_ends i /\ x \in i)
diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v
index 913b38a58c..d8a73b0637 100644
--- a/theories/probability_theory/beta_distribution.v
+++ b/theories/probability_theory/beta_distribution.v
@@ -494,11 +494,10 @@ Proof.
 move=> mU; rewrite /beta_pdf.
 under eq_integral do rewrite EFinM/=.
 rewrite ge0_integralZr//=.
-- apply/measurable_funTS/measurableT_comp => //.
-  by apply/measurable_restrict => //=; rewrite setTI; exact: measurable_XMonemX.
 - move=> x Ux; rewrite patchE; case: ifPn => //; rewrite inE/= => x01.
   by rewrite lee_fin XMonemX_ge0.
-- by rewrite lee_fin invr_ge0// beta_fun_ge0.
+- apply/measurable_funTS/measurableT_comp => //.
+  by apply/measurable_restrict => //=; rewrite setTI; exact: measurable_XMonemX.
 - by rewrite /beta_prob/= /mscale/= muleC.
 Qed.
 
diff --git a/theories/probability_theory/independence.v b/theories/probability_theory/independence.v
index 2743dd0047..96b881e56c 100644
--- a/theories/probability_theory/independence.v
+++ b/theories/probability_theory/independence.v
@@ -584,17 +584,13 @@ rewrite fubini_tonelli1//=.
 rewrite /fubini_F/=.
 rewrite [ltLHS](_ : _ = (\int[distribution P X]_x `|x|%:E) *
                         \int[distribution P Y]_y `|y|%:E).
-  rewrite -ge0_integralZr//=.
-    exact/measurable_EFinP.
-    exact: integral_ge0.
+  rewrite -ge0_integralZr//=; first exact/measurable_EFinP.
   apply: eq_integral => x _.
-  rewrite -ge0_integralZl//=.
-    exact/measurable_EFinP.
+  rewrite -ge0_integralZl//=; first exact/measurable_EFinP.
   by under eq_integral do rewrite normrM.
 rewrite ge0_integral_distribution//=; first exact/measurable_EFinP.
 rewrite ge0_integral_distribution//=; first exact/measurable_EFinP.
-rewrite lte_mul_pinfty//.
-- exact: integral_ge0.
+rewrite lte_mul_pinfty ?integral_ge0//.
 - apply: integrable_fin_num => //=.
   by move/Lfun1_integrable : iX => /integrable_abse.
 - apply: integrable_lty => //.
diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v
index e55cae516b..a2df3f5dc2 100644
--- a/theories/probability_theory/normal_distribution.v
+++ b/theories/probability_theory/normal_distribution.v
@@ -251,10 +251,10 @@ Proof.
 move=> s0; rewrite /normal_peak invrK.
 rewrite -mulrnAr -[in RHS]mulr_natr sqrtrM ?(sqrtrM 2) ?sqr_ge0 ?pi_ge0// !EFinM.
 rewrite muleCA ge0_integralZr//=.
+- by move=> x _; rewrite lee_fin mulr_ge0//= ?gauss_fun_ge0// F'E/= invr_ge0.
 - rewrite F'E; apply/measurable_EFinP/measurable_funM => //.
   apply/measurableT_comp => //; first exact: measurable_gauss_fun.
   by apply: measurable_funM => //; exact: measurable_funD.
-- by move=> x _; rewrite lee_fin mulr_ge0//= ?gauss_fun_ge0// F'E/= invr_ge0.
 congr *%E; last by rewrite -(mulr_natr (_ ^+ 2)) sqrtrM ?sqr_ge0.
 rewrite -increasing_ge0_integration_by_substitutionT//.
 - move=> x y xy; rewrite /F ltr_pM2r ?ltr_leB ?gt_eqF//.
@@ -720,13 +720,12 @@ Lemma normal_probD2 (y m1 m2 s1 s2 : R) : s1 != 0%R -> s2 != 0%R ->
   \int[mu]_z (normal_fun (m1 + z) s1 y * normal_fun m2 s2 z)%:E.
 Proof.
 move=> s10 s20; rewrite -ge0_integralZl//=.
+- by move=> z _; rewrite lee_fin mulr_ge0// expR_ge0.
 - apply/measurable_EFinP => //=; apply: measurable_funM => //=.
   + rewrite /normal_fun. (* TODO: lemma? *)
     under eq_fun do rewrite -(sqrrN (y - _)) opprB (addrC m1) -addrA -opprB.
     exact: measurable_normal_fun.
   + exact: measurable_normal_fun.
-- by move=> z _; rewrite lee_fin mulr_ge0// expR_ge0.
-- by rewrite lee_fin mulr_ge0// ?normal_peak_ge0.
 apply: eq_integral => /= z _.
 by rewrite 2?normal_pdfE// /normal_pdf0 mulrACA.
 Qed.
@@ -806,9 +805,8 @@ transitivity (((Num.sqrt S1 * Num.sqrt S2 * pi *+ 2)^-1)%:E
   rewrite lt0r_neq0// invr_gt0 sqrtr_gt0 pmulrn_lgt0// mulr_gt0// ?pi_gt0//.
   by rewrite exprn_even_gt0//= lt0r_neq0// sqrtr_gt0.
 rewrite ge0_integralZl//=.
-- by apply/measurable_EFinP; exact: measurable_normal_pdf.
 - by move=> x _; rewrite lee_fin; exact: normal_pdf_ge0.
-- by rewrite lee_fin invr_ge0; exact: normal_peak_ge0.
+- by apply/measurable_EFinP; exact: measurable_normal_pdf.
 rewrite integral_normal_pdf mule1 -EFinM; congr EFin.
 rewrite -invfM; congr GRing.inv.
 rewrite -sqrtrM ?sqr_ge0// /normal_peak sqr_sqrtr; first by rewrite ltW.
@@ -942,10 +940,9 @@ have step U : measurable U ->
   rewrite integral_normal_prob ?integrable_normal_pdf_likelihood//=.
   under eq_integral => t _ do
     rewrite -EFinM (normal_pdf_conjugate m0 x t s0_neq0 s_neq0) EFinM.
-  rewrite -/K ge0_integralZl_EFin //=.
+  rewrite -/K ge0_integralZl//=.
   - by move=> t _; rewrite lee_fin; exact: normal_pdf_ge0.
   - by apply/measurable_EFinP/measurable_funTS; exact: measurable_normal_pdf.
-  - exact: ltW.
 rewrite (step _ mV) (step _ measurableT) probability_setT mule1.
 by rewrite muleAC divee // mul1e.
 Qed.
diff --git a/theories/probability_theory/uniform_distribution.v b/theories/probability_theory/uniform_distribution.v
index 409fb2afa7..db21ea3dde 100644
--- a/theories/probability_theory/uniform_distribution.v
+++ b/theories/probability_theory/uniform_distribution.v
@@ -139,7 +139,6 @@ Let integral_uniform_indic E : measurable E ->
 Proof.
 move=> mE; rewrite integral_indic//= /uniform_prob setIT -ge0_integralZl//=.
 - exact/measurable_EFinP/measurable_indic.
-- by rewrite lee_fin invr_ge0// ltW// subr_gt0.
 rewrite [LHS]integral_mkcond/= [RHS]integral_mkcond/=.
 apply: eq_integral => x _; rewrite !patchE; case: ifPn => xE.
   case: ifPn.
@@ -161,9 +160,8 @@ rewrite [LHS]ge0_integral_fsum//.
 - by move=> r; exact/measurable_EFinP/measurableT_comp.
 - by move=> n x _; rewrite EFinM nnfun_muleindic_ge0.
 rewrite -[RHS]ge0_integralZl//.
-- exact/measurable_EFinP/measurable_funTS.
 - by move=> x _; rewrite lee_fin.
-- by rewrite lee_fin invr_ge0// ltW// subr_gt0.
+- exact/measurable_EFinP/measurable_funTS.
 under [RHS]eq_integral.
   move=> x xD; rewrite fimfunE -fsumEFin// ge0_mule_fsumr.
     by move=> r; rewrite EFinM nnfun_muleindic_ge0.
@@ -173,9 +171,8 @@ rewrite [RHS]ge0_integral_fsum//.
 - move=> n x _; rewrite EFinM mule_ge0//; last by rewrite nnfun_muleindic_ge0.
   by rewrite lee_fin invr_ge0// ltW// subr_gt0.
 apply: eq_fsbigr => r _; rewrite ge0_integralZl//.
-- exact/measurable_EFinP/measurableT_comp.
 - by move=> t _; rewrite nnfun_muleindic_ge0.
-- by rewrite lee_fin invr_ge0// ltW// subr_gt0.
+- exact/measurable_EFinP/measurableT_comp.
 - by rewrite !integralZl_indic_nnsfun//= integral_uniform_indic// muleCA.
 Qed.