naming conventions

CHANGELOG_UNRELEASED.md

@@ -8,6 +8,23 @@
 
 ### Renamed
 
+- in `constructive_ereal.v`:
+  + `lee_addl` -> `leeDl`
+  + `lee_addr` -> `leeDr`
+  + `lee_add2l` -> `leeD2l`
+  + `lee_add2r` -> `leeD2r`
+  + `lee_add` -> `leeD`
+  + `lee_sub` -> `leeB`
+  + `lee_add2lE` -> `leeD2lE`
+  + `lte_add2lE` -> `lteD2lE`
+  + `lee_oppl` -> `leeNl`
+  + `lee_oppr` -> `leeNr`
+  + `lte_oppr` -> `lteNr`
+  + `lte_oppl` -> `lteNl`
+  + `lte_add` -> `lteD`
+  + `lte_addl` -> `lteDl`
+  + `lte_addr` -> `lteDr`
+
 ### Generalized
 
 ### Deprecated

theories/ereal.v

@@ -422,16 +422,16 @@ Qed.
 
 Lemma lb_ereal_inf S M : lbound S M -> M <= ereal_inf S.
 Proof.
-move=> SM; rewrite /ereal_inf lee_oppr; apply ub_ereal_sup => x [y Sy <-{x}].
-by rewrite lee_oppl oppeK; apply SM.
+move=> SM; rewrite /ereal_inf leeNr; apply ub_ereal_sup => x [y Sy <-{x}].
+by rewrite leeNl oppeK; apply SM.
 Qed.
 
 Lemma ub_ereal_sup_adherent S (e : R) : (0 < e)%R ->
   ereal_sup S \is a fin_num -> exists2 x, S x & (ereal_sup S - e%:E < x).
 Proof.
 move=> e0 Sr; have : ~ ubound S (ereal_sup S - e%:E).
   move/ub_ereal_sup; apply/negP.
-  by rewrite -ltNge lte_subl_addr // lte_addl // lte_fin.
+  by rewrite -ltNge lte_subl_addr // lteDl // lte_fin.
 move/asboolP; rewrite asbool_neg; case/existsp_asboolPn => /= x.
 by rewrite not_implyE => -[? ?]; exists x => //; rewrite ltNge; apply/negP.
 Qed.
@@ -440,7 +440,7 @@ Lemma lb_ereal_inf_adherent S (e : R) : (0 < e)%R ->
   ereal_inf S \is a fin_num -> exists2 x, S x & (x < ereal_inf S + e%:E).
 Proof.
 move=> e0; rewrite fin_numN => /(ub_ereal_sup_adherent e0)[x []].
-move=> y Sy <-; rewrite -lte_oppr => /lt_le_trans ex; exists y => //.
+move=> y Sy <-; rewrite -lteNr => /lt_le_trans ex; exists y => //.
 by apply: ex; rewrite fin_num_oppeD// oppeK.
 Qed.
 
@@ -452,8 +452,8 @@ Qed.
 
 Lemma ereal_inf_lt S x : ereal_inf S < x -> exists2 y, S y & y < x.
 Proof.
-rewrite lte_oppl => /ereal_sup_gt[_ [y Sy <-]].
-by rewrite lte_oppl oppeK => xlty; exists y.
+rewrite lteNl => /ereal_sup_gt[_ [y Sy <-]].
+by rewrite lteNl oppeK => xlty; exists y.
 Qed.
 
 End ereal_supremum.
@@ -528,7 +528,7 @@ Qed.
 
 Lemma ereal_inf_lb S : lbound S (ereal_inf S).
 Proof.
-by move=> x Sx; rewrite /ereal_inf lee_oppl; apply ereal_sup_ub; exists x.
+by move=> x Sx; rewrite /ereal_inf leeNl; apply ereal_sup_ub; exists x.
 Qed.
 
 Lemma ereal_inf_le S x : (exists2 y, S y & y <= x) -> ereal_inf S <= x.
@@ -838,19 +838,19 @@ case: x => [r /=| |].
 - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
     exists (-%E @` S).
       exists (- M)%R; rewrite realN Mreal; split => // x Mx.
-      by exists (- x); [apply MS; rewrite lte_oppl | rewrite oppeK].
+      by exists (- x); [apply MS; rewrite lteNl | rewrite oppeK].
     rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
     by exists (- x); [exists x | rewrite oppeK].
   exists (- M)%R; rewrite realN; split => // y yM.
-  exists (- y); by [apply Mx; rewrite lte_oppr|rewrite oppeK].
+  exists (- y); by [apply Mx; rewrite lteNr|rewrite oppeK].
 - rewrite predeqE => S; split=> [[M [Mreal MS]]|[x [M [Mreal Mx]] <-]].
     exists (-%E @` S).
       exists (- M)%R; rewrite realN Mreal; split => // x Mx.
-      by exists (- x); [apply MS; rewrite lte_oppr | rewrite oppeK].
+      by exists (- x); [apply MS; rewrite lteNr | rewrite oppeK].
     rewrite predeqE => x; split=> [[y [z Sz <- <-]]|Sx]; first by rewrite oppeK.
     by exists (- x); [exists x | rewrite oppeK].
   exists (- M)%R; rewrite realN; split => // y yM.
-  exists (- y); by [apply Mx; rewrite lte_oppl|rewrite oppeK].
+  exists (- y); by [apply Mx; rewrite lteNl|rewrite oppeK].
 Qed.
 
 Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) :

theories/esum.v

@@ -134,14 +134,14 @@ Lemma esumD [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) :
 Proof.
 move=> ag0 bg0; apply/eqP; rewrite eq_le; apply/andP; split.
   rewrite ub_ereal_sup//= => x [X [finX XI]] <-; rewrite fsbig_split//=.
-  by rewrite lee_add// ereal_sup_ub//=; exists X.
+  by rewrite leeD// ereal_sup_ub//=; exists X.
 wlog : a b ag0 bg0 / \esum_(i in I) a i \isn't a fin_num => [saoo|]; last first.
   move=> /fin_numPn[->|/[dup] aoo ->]; first by rewrite leNye.
   rewrite (@le_trans _ _ +oo)//; first by rewrite /adde/=; case: esum.
   rewrite leye_eq; apply/eqP/eq_infty => y; rewrite esum_ge//.
   have : y%:E < \esum_(i in I) a i by rewrite aoo// ltry.
   move=> /ereal_sup_gt[_ [X [finX XI]] <-] /ltW yle; exists X => //=.
-  rewrite (le_trans yle)// fsbig_split// lee_addl// fsume_ge0// => // i.
+  rewrite (le_trans yle)// fsbig_split// leeDl// fsume_ge0// => // i.
   by move=> /XI; exact: bg0.
 case: (boolP (\esum_(i in I) a i \is a fin_num)) => sa; last exact: saoo.
 case: (boolP (\esum_(i in I) b i \is a fin_num)) => sb; last first.
@@ -156,7 +156,7 @@ have saX : \sum_(i \in X) a i \is a fin_num.
 rewrite lee_subr_addr// addeC -lee_subr_addr// ub_ereal_sup//= => _ [Y [finY YI]] <-.
 rewrite lee_subr_addr// addeC esum_ge//; exists (X `|` Y).
   by split; [rewrite finite_setU|rewrite subUset].
-rewrite fsbig_split ?finite_setU//= lee_add// lee_fsum_nneg_subset//= ?finite_setU//.
+rewrite fsbig_split ?finite_setU//= leeD// lee_fsum_nneg_subset//= ?finite_setU//.
 - exact/subsetP/subsetUl.
 - by move=> x; rewrite !inE in_setU andb_orr andNb/= => /andP[_] /[!inE] /YI/ag0.
 - exact/subsetP/subsetUr.
@@ -250,7 +250,7 @@ apply: (@le_trans _ _
   rewrite (_ : [fset x | x in Y & x \in X] = Y `&` fset_set X)%fset; last first.
     by apply/fsetP => x; rewrite 2!inE/= in_fset_set.
   rewrite (fsetIidPr _).
-    rewrite fsbig_finite// lee_addl// big_seq sume_ge0//=.
+    rewrite fsbig_finite// leeDl// big_seq sume_ge0//=.
     move=> [x y] /imfsetP[[x1 y1]] /[!inE] /andP[] /imfset2P[x2]/= /[!inE].
     rewrite andbT in_fset_set//; last exact: finite_set_fst.
     move=> /[!inE] x2X [y2] /[!inE] /andP[] /[!in_fset_set]; last first.
@@ -281,7 +281,7 @@ Lemma lee_sum_fset_nat (R : realDomainType)
 Proof.
 move=> f0 Fn; rewrite [leRHS](bigID (mem F))/=.
 suff -> : \sum_(0 <= i < n | P i && (i \in F)) f i = \sum_(i <- F | P i) f i.
-  by rewrite lee_addl ?sume_ge0// => i /andP[/f0].
+  by rewrite leeDl ?sume_ge0// => i /andP[/f0].
 rewrite -big_filter -[RHS]big_filter; apply: perm_big.
 rewrite uniq_perm ?filter_uniq ?index_iota ?iota_uniq ?fset_uniq//.
 move=> i; rewrite ?mem_filter.
@@ -462,7 +462,7 @@ Implicit Types (D : set T) (f : T -> \bar R).
 Lemma summable_pinfty D f : summable D f -> forall x, D x -> `| f x | < +oo.
 Proof.
 move=> Dfoo x Dx; apply: le_lt_trans Dfoo.
-rewrite (esumID [set x])// setI1 mem_set// esum_set1// lee_addl//.
+rewrite (esumID [set x])// setI1 mem_set// esum_set1// leeDl//.
 exact: esum_ge0.
 Qed.
 
@@ -489,13 +489,13 @@ Proof. by move=> Df; rewrite summableN; exact: summableD. Qed.
 Lemma summable_funepos D f : summable D f -> summable D f^\+.
 Proof.
 apply: le_lt_trans; apply le_esum => t Dt.
-by rewrite -/((abse \o f) t) fune_abse gee0_abs// lee_addl.
+by rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDl.
 Qed.
 
 Lemma summable_funeneg D f : summable D f -> summable D f^\-.
 Proof.
 apply: le_lt_trans; apply le_esum => t Dt.
-by rewrite -/((abse \o f) t) fune_abse gee0_abs// lee_addr.
+by rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDr.
 Qed.
 
 End summable_lemmas.
@@ -620,9 +620,9 @@ have /eqP : esum D (f \- g)^\+ + esum_posneg D g = esum D (f \- g)^\- + esum_pos
     by move=> t Dt; rewrite le_maxr lexx orbT.
     by move=> t Dt; rewrite le_maxr lexx orbT.
   apply eq_esum => i Di; have [fg|fg] := leP 0 (f i - g i).
-    rewrite max_r 1?lee_oppl ?oppe0// add0e subeK//.
+    rewrite max_r 1?leeNl ?oppe0// add0e subeK//.
     by rewrite fin_num_abs (summable_pinfty Dg).
-  rewrite add0e max_l; last by rewrite lee_oppr oppe0 ltW.
+  rewrite add0e max_l; last by rewrite leeNr oppe0 ltW.
   rewrite fin_num_oppeB//; last by rewrite fin_num_abs (summable_pinfty Dg).
   by rewrite -addeA addeCA addeA subeK// fin_num_abs (summable_pinfty Df).
 rewrite [X in _ == X -> _]addeC -sube_eq; last 2 first.

theories/hoelder.v

@@ -467,7 +467,7 @@ rewrite [leRHS](_ : _ = ('N_p%:E[f] + 'N_p%:E[g]) *
     - rewrite fin_num_poweR// -powR_Lnorm ?gt_eqF// fin_num_poweR//.
       by rewrite ge0_fin_numE ?Lnorm_ge0.
     - by rewrite ge0_adde_def// inE Lnorm_ge0.
-  apply: lee_add.
+  apply: leeD.
   - pose h := (@powR R ^~ (p - 1) \o normr \o (f \+ g))%R; pose i := (f \* h)%R.
     rewrite [leLHS](_ : _ = 'N_1[i]%R); last first.
       rewrite Lnorm1; apply: eq_integral => x _.

theories/lebesgue_integral.v

@@ -840,7 +840,7 @@ Proof. by split=> x; rewrite subr_ge0 fg. Qed.
 Lemma le_sintegral : (sintegral m f <= sintegral m g)%E.
 Proof.
 have gfgf : g =1 f \+ (g \- f) by move=> x /=; rewrite addrC subrK.
-by rewrite (eq_sintegral _ _ gfgf) sintegralD// lee_addl // sintegral_ge0.
+by rewrite (eq_sintegral _ _ gfgf) sintegralD// leeDl // sintegral_ge0.
 Qed.
 
 End le_sintegral.
@@ -1215,7 +1215,7 @@ rewrite le_eqVlt => /predU1P[|] mufoo; last first.
   have : forall x, cvgn (g^~ x) -> (G x <= limn (g ^~ x))%R.
     move=> x cg; rewrite -lee_fin -(EFin_lim cg).
     by have /cvg_lim gxfx := @gf x; rewrite (le_trans (Gf _))// gxfx.
-  move=> /(nd_sintegral_lim_lemma mu nd_g)/(lee_add2r e%:num%:E).
+  move=> /(nd_sintegral_lim_lemma mu nd_g)/(leeD2r e%:num%:E).
   by apply: le_trans; exact: ltW.
 suff : limn (sintegral mu \o g) = +oo.
   by move=> ->; rewrite -ge0_integralTE// mufoo.
@@ -1873,7 +1873,7 @@ have -> : A `\` D = (A `\` K) `|` (K `\` D).
 apply: le_lt_trans.
   apply: measureU2; apply: measurableD => //; apply: closed_measurable.
   by apply: compact_closed; first exact: Rhausdorff.
-by rewrite [_ eps]splitr EFinD lte_add.
+by rewrite [_ eps]splitr EFinD lteD.
 Qed.
 
 End lusin.
@@ -2853,7 +2853,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
       by rewrite measure_addE; exact: nneseries_split.
     rewrite integral_measure_add//; congr (_ + _).
     by rewrite -ge0_integral_measure_sum.
-  by apply: lee_addl; exact: integral_ge0.
+  by apply: leeDl; exact: integral_ge0.
 rewrite ge0_integralE//=; apply: ub_ereal_sup => /= _ [g /= gf] <-.
 rewrite -integralT_nnsfun (integral_measure_series_nnsfun _ mD).
 apply: lee_nneseries => n _.
@@ -2906,7 +2906,7 @@ move=> mf f0 AB; rewrite -(setDUK AB) integral_setU//; last 4 first.
   - by rewrite setDUK.
   - by move=> x; rewrite setDUK//; exact: f0.
   - by rewrite disj_set2E setDIK.
-by apply: lee_addl; apply: integral_ge0 => x [Bx _]; exact: f0.
+by apply: leeDl; apply: integral_ge0 => x [Bx _]; exact: f0.
 Qed.
 
 Lemma integral_set0 (f : T -> \bar R) : \int[mu]_(x in set0) f x = 0.
@@ -3071,8 +3071,8 @@ rewrite ge0_integralD // in foo; last 2 first.
 - exact: measurable_funepos.
 - exact: measurable_funeneg.
 apply: ltpinfty_adde_def.
-- by apply: le_lt_trans foo; rewrite lee_addl// integral_ge0.
-- by rewrite inE (@le_lt_trans _ _ 0)// lee_oppl oppe0 integral_ge0.
+- by apply: le_lt_trans foo; rewrite leeDl// integral_ge0.
+- by rewrite inE (@le_lt_trans _ _ 0)// leeNl oppe0 integral_ge0.
 Qed.
 
 Lemma integrable_funepos f : mu_int f -> mu_int f^\+.
@@ -3082,7 +3082,7 @@ move=> /integrableP[Df foo]; apply/integrableP; split.
 apply: le_lt_trans foo; apply: ge0_le_integral => //.
 - by apply/measurableT_comp => //; exact: measurable_funepos.
 - exact/measurableT_comp.
-- by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// lee_addl.
+- by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDl.
 Qed.
 
 Lemma integrable_funeneg f : mu_int f -> mu_int f^\-.
@@ -3092,7 +3092,7 @@ move=> /integrableP[Df foo]; apply/integrableP; split.
 apply: le_lt_trans foo; apply: ge0_le_integral => //.
 - by apply/measurableT_comp => //; exact: measurable_funeneg.
 - exact/measurableT_comp.
-- by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// lee_addr.
+- by move=> t Dt; rewrite -/((abse \o f) t) fune_abse gee0_abs// leeDr.
 Qed.
 
 Lemma integral_funeneg_lt_pinfty f : mu_int f ->
@@ -3103,9 +3103,9 @@ move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //.
 - exact: measurableT_comp.
 - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0.
     rewrite lee0_abs// /funeneg.
-    by move: fx0; rewrite -{1}oppe0 -lee_oppr => /max_idPl ->.
+    by move: fx0; rewrite -{1}oppe0 -leeNr => /max_idPl ->.
   rewrite gee0_abs// /funeneg.
-  by move: (fx0); rewrite -{1}oppe0 -lee_oppl => /max_idPr ->.
+  by move: (fx0); rewrite -{1}oppe0 -leeNl => /max_idPr ->.
 Qed.
 
 Lemma integral_funepos_lt_pinfty f : mu_int f ->
@@ -3116,7 +3116,7 @@ move=> /integrableP[mf]; apply: le_lt_trans; apply: ge0_le_integral => //.
 - exact: measurableT_comp.
 - move=> x Dx; have [fx0|/ltW fx0] := leP (f x) 0.
     rewrite lee0_abs// /funepos.
-    by move: (fx0) => /max_idPr ->; rewrite -lee_oppr oppe0.
+    by move: (fx0) => /max_idPr ->; rewrite -leeNr oppe0.
   by rewrite gee0_abs// /funepos; move: (fx0) => /max_idPl ->.
 Qed.
 
@@ -3129,7 +3129,7 @@ rewrite fin_numElt; apply/andP; split.
 case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
 - exact/measurable_funeneg.
 - exact/measurableT_comp.
-- by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) lee_addr.
+- by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) leeDr.
 Qed.
 
 Lemma integrable_pos_fin_num f :
@@ -3141,7 +3141,7 @@ rewrite fin_numElt; apply/andP; split.
 case: fi => mf; apply: le_lt_trans; apply: ge0_le_integral => //.
 - exact/measurable_funepos.
 - exact/measurableT_comp.
-- by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) lee_addl.
+- by move=> x Dx; rewrite -/((abse \o f) x) (fune_abse f) leeDl.
 Qed.
 
 End integrable_theory.
@@ -3981,15 +3981,15 @@ Lemma integral_fune_lt_pinfty (f : T -> \bar R) :
 Proof.
 move=> intf; rewrite (funeposneg f) integralB//;
   [|exact: integrable_funepos|exact: integrable_funeneg].
-rewrite lte_add_pinfty ?integral_funepos_lt_pinfty// lte_oppl ltNye_eq.
+rewrite lte_add_pinfty ?integral_funepos_lt_pinfty// lteNl ltNye_eq.
 by rewrite integrable_neg_fin_num.
 Qed.
 
 Lemma integral_fune_fin_num (f : T -> \bar R) :
   mu.-integrable D f -> \int[mu]_(x in D) f x \is a fin_num.
 Proof.
 move=> h; apply/fin_numPlt; rewrite integral_fune_lt_pinfty// andbC/= -/(- +oo).
-rewrite lte_oppl -integralN; first exact/integral_fune_lt_pinfty/integrableN.
+rewrite lteNl -integralN; first exact/integral_fune_lt_pinfty/integrableN.
 by rewrite fin_num_adde_defl// fin_numN integrable_neg_fin_num.
 Qed.
 
@@ -4169,19 +4169,19 @@ move: (f_f Dx); case: (f x) => [r|/=|/=].
 - move/cvgeyPge/(_ (fine (g x) + 1)%R) => [n _]/(_ _ (leqnn n))/= h.
   have : (fine (g x) + 1)%:E <= g x.
     by rewrite (le_trans h)// (le_trans _ (absfg n Dx))// lee_abs.
-  by case: (g x) (fing Dx) => [r _| |]//; rewrite leNgt EFinD lte_addl ?lte01.
+  by case: (g x) (fing Dx) => [r _| |]//; rewrite leNgt EFinD lteDl ?lte01.
 - move/cvgeNyPle/(_ (- (fine (g x) + 1))%R) => [n _]/(_ _ (leqnn n)) h.
   have : (fine (g x) + 1)%:E <= g x.
-    move: h; rewrite EFinN lee_oppr => /le_trans ->//.
+    move: h; rewrite EFinN leeNr => /le_trans ->//.
     by rewrite (le_trans _ (absfg n Dx))// -abseN lee_abs.
-  by case: (g x) (fing Dx) => [r _| |]//; rewrite leNgt EFinD lte_addl ?lte01.
+  by case: (g x) (fing Dx) => [r _| |]//; rewrite leNgt EFinD lteDl ?lte01.
 Qed.
 
 Let gg_ n x : D x -> 0 <= 2%:E * g x - g_ n x.
 Proof.
 move=> Dx; rewrite subre_ge0; last by rewrite fin_numM// fing.
 rewrite -(fineK (fing Dx)) -EFinM mulr_natl mulr2n /g_.
-rewrite (le_trans (lee_abs_sub _ _))// [in leRHS]EFinD lee_add//.
+rewrite (le_trans (lee_abs_sub _ _))// [in leRHS]EFinD leeD//.
   by rewrite fineK// ?fing// absfg.
 have f_fx : `|(f_ n x)| @[n --> \oo] --> `|f x| by apply: cvg_abse; exact: f_f.
 move/cvg_lim : (f_fx) => <-//.
@@ -4235,7 +4235,7 @@ rewrite [X in _ <= X -> _](_ : _ = \int[mu]_(x in D) (2%:E * g x)  + -
       - by move=> x Dx; rewrite /= abse_id.
   rewrite limn_einf_shift // -limn_einfN; congr (_ + limn_einf _).
   by rewrite funeqE => n /=; rewrite -integral_ge0N// => x Dx; rewrite /g_.
-rewrite addeC -lee_subl_addr// subee// lee_oppr oppe0 => lim_ge0.
+rewrite addeC -lee_subl_addr// subee// leeNr oppe0 => lim_ge0.
 by apply/limn_esup_le_cvg => // n; rewrite integral_ge0// => x _; rewrite /g_.
 Qed.
 
@@ -5066,7 +5066,7 @@ exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans.
 rewrite integralD//; first last.
 - by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB.
 - by apply: integrable_abse; under eq_fun do rewrite EFinB; apply: integrableB.
-rewrite EFinD lte_add// -(setDKU AE) integral_setU => //; first last.
+rewrite EFinD lteD// -(setDKU AE) integral_setU => //; first last.
 - by rewrite /disj_set setDKI.
 - rewrite setDKU //; do 2 apply: measurableT_comp => //.
   exact: measurable_funB.
@@ -5507,7 +5507,7 @@ apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //.
   - apply: measurableT_comp => //.
     by apply: measurable_funepos => //; exact: measurableT_comp.
   - by apply: measurableT_comp => //; exact/measurableT_comp.
-  - by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addl.
+  - by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl.
 Qed.
 
 Let integrable_Fminus : m1.-integrable setT Fminus.
@@ -5523,7 +5523,7 @@ apply: le_lt_trans (fubini1a.1 imf); apply: ge0_le_integral => //.
   + apply: measurableT_comp => //; apply: measurable_funeneg => //.
     exact: measurableT_comp.
   + by apply: measurableT_comp => //; exact: measurableT_comp.
-  + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addr.
+  + by move=> y _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr.
 Qed.
 
 Lemma integrable_fubini_F : m1.-integrable setT F.
@@ -5562,7 +5562,7 @@ apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //.
   - apply: measurableT_comp => //.
     by apply: measurable_funepos => //; exact: measurableT_comp.
   - by apply: measurableT_comp => //; exact: measurableT_comp.
-  - by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addl.
+  - by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDl.
 Qed.
 
 Let integrable_Gminus : m2.-integrable setT Gminus.
@@ -5578,7 +5578,7 @@ apply: le_lt_trans (fubini1b.1 imf); apply: ge0_le_integral => //.
   + apply: measurableT_comp => //.
     by apply: measurable_funeneg => //; exact: measurableT_comp.
   + by apply: measurableT_comp => //; exact: measurableT_comp.
-  + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse lee_addr.
+  + by move=> x _; rewrite gee0_abs// -/((abse \o f) (x, y)) fune_abse leeDr.
 Qed.
 
 Lemma fubini1 : \int[m1]_x F x = \int[m1 \x m2]_z f z.