diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 197692e10..542d716f8 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -39,6 +39,10 @@
 - in `realfun.v`:
   + lemma `nondecreasing_at_left_is_cvgr`
 
+- in `constructive_ereal.v`:
+  + lemmas `lteD2rE`, `leeD2rE`
+  + lemmas `lte_dD2rE`, `lee_dD2rE`
+
 ### Changed
 
 - in `topology.v`:
@@ -87,8 +91,43 @@
 - in `measure.v`:
   + `setD_closed` -> `setSD_closed`
 
+- in `constructive_ereal.v`:
+  + `lte_dadd` -> `lte_dD`
+  + `lee_daddl` -> `lee_dDl`
+  + `lee_daddr` -> `lee_dDr`
+  + `gee_daddl` -> `gee_dDl`
+  + `gee_daddr` -> `gee_dDr`
+  + `lte_daddl` -> `lte_dDl`
+  + `lte_daddr` -> `lte_dDr`
+  + `gte_dsubl` -> `gte_dBl`
+  + `gte_dsubr` -> `gte_dBr`
+  + `gte_daddl` -> `gte_dDl`
+  + `gte_daddr` -> `gte_dDr`
+  + `lee_dadd2lE` -> `lee_dD2lE`
+  + `lte_dadd2lE` -> `lte_dD2lE`
+  + `lee_dadd2rE` -> `lee_dD2rE`
+  + `lee_dadd2l` -> `lee_dD2l`
+  + `lee_dadd2r` -> `lee_dD2r`
+  + `lee_dadd` -> `lee_dD`
+  + `lee_dsub` -> `lee_dB`
+  + `lte_dsubl_addr` -> `lte_dBlDr`
+  + `lte_dsubl_addl` -> `lte_dBlDl`
+  + `lte_dsubr_addr` -> `lte_dBrDr`
+  + `lte_dsubr_addl` -> `lte_dBrDl`
+  + `gte_opp` -> `gteN`
+  + `gte_dopp` -> `gte_dN`
+  + `lte_le_add` -> `lte_leD`
+  + `lee_lt_add` -> `lee_ltD`
+  + `lte_le_dadd` -> `lte_le_dD`
+  + `lee_lt_dadd` -> `lee_lt_dD`
+  + `lte_le_sub` -> `lte_leB`
+  + `lte_le_dsub` -> `lte_le_dB`
+
 ### Generalized
 
+- in `constructive_ereal.v`:
+  + lemmas `leeN2`, `lteN2` generalized from `realDomainType` to `numDomainType`
+
 ### Deprecated
 
 - in `reals.v`:
@@ -96,6 +135,9 @@
   + `le_floor` (use `Num.Theory.floor_le` instead)
   + `le_ceil` (use `ceil_ge` instead)
 
+- in `constructive_ereal.v`:
+  + lemmas `lte_opp2`, `lee_opp2` (use `lteN2`, `leeN2` instead)
+
 ### Removed
 
 - in `reals.v`:
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 831e91b69..b5a5822f6 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -620,6 +620,20 @@ Lemma mule2n x : x *+ 2 = x + x. Proof. by []. Qed.
 
 Lemma expe2 x : x ^+ 2 = x * x. Proof. by []. Qed.
 
+Lemma leeN2 : {mono @oppe R : x y /~ x <= y}.
+Proof.
+move=> x y; case: x y => [?||] [?||] //; first by rewrite !lee_fin !lerN2.
+  by rewrite /Order.le/= realN.
+by rewrite /Order.le/= realN.
+Qed.
+
+Lemma lteN2 : {mono @oppe R : x y /~ x < y}.
+Proof.
+move=> x y; case: x y => [?||] [?||] //; first by rewrite !lte_fin !ltrN2.
+  by rewrite /Order.lt/= realN.
+by rewrite /Order.lt/= realN.
+Qed.
+
 End ERealOrderTheory.
 #[global] Hint Resolve leeN10 lteN10 : core.
 
@@ -1191,7 +1205,7 @@ Qed.
 Lemma mule_lt0_gt0 x y : x < 0 -> 0 < y -> x * y < 0.
 Proof. by move=> x0 y0; rewrite muleC mule_gt0_lt0. Qed.
 
-Lemma gte_opp x : 0 < x -> - x < x.
+Lemma gteN x : 0 < x -> - x < x.
 Proof. by case: x => //= r; rewrite !lte_fin; apply: gtrN. Qed.
 
 Lemma realMe x y : (0%E >=< x)%O -> (0%E >=< y)%O -> (0%E >=< x * y)%O.
@@ -1244,6 +1258,9 @@ Notation mine := (@Order.min ereal_display _).
 Notation "@ 'mine' R" := (@Order.min ereal_display R)
   (at level 10, R at level 8, only parsing) : function_scope.
 
+#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `gteN`")]
+Notation gte_opp := gteN (only parsing).
+
 Module DualAddTheoryNumDomain.
 
 Section DualERealArithTh_numDomainType.
@@ -1459,7 +1476,7 @@ move=> u0 l; rewrite dual_sumeE oppe_le0 sume_ge0 // => t Pt.
 rewrite oppe_ge0; exact: u0.
 Qed.
 
-Lemma gte_dopp (r : \bar^d R) : (0 < r)%E -> (- r < r)%E.
+Lemma gte_dN (r : \bar^d R) : (0 < r)%E -> (- r < r)%E.
 Proof. by case: r => //= r; rewrite !lte_fin; apply: gtrN. Qed.
 
 Lemma ednatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar^d R.
@@ -1490,6 +1507,9 @@ Qed.
 
 End DualERealArithTh_numDomainType.
 
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dN`")]
+Notation gte_dopp := gte_dN (only parsing).
+
 End DualAddTheoryNumDomain.
 
 Section ERealArithTh_realDomainType.
@@ -1727,8 +1747,6 @@ have := mule_eq_pinfty x (- y); rewrite muleN eqe_oppLR => ->.
 by rewrite !eqe_oppLR lteNr lteNl oppe0 (orbC _ ((x == -oo) && _)).
 Qed.
 
-Lemma lteN2 x y : (- x < - y) = (y < x). Proof. by rewrite lteNl oppeK. Qed.
-
 Lemma lteD a b x y : a < b -> x < y -> a + x < b + y.
 Proof.
 move: a b x y=> [a| |] [b| |] [x| |] [y| |]; rewrite ?(ltry,ltNyr)//.
@@ -1783,6 +1801,9 @@ move: a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(ltry, ltNyr)//.
 by rewrite !lte_fin ltrD2l.
 Qed.
 
+Lemma lteD2rE x a b : x \is a fin_num -> (a + x < b + x) = (a < b).
+Proof. by rewrite -!(addeC x); exact: lteD2lE. Qed.
+
 Lemma leeD2l x a b : a <= b -> x + a <= x + b.
 Proof.
 move: a b x => -[a [b [x /=|//|//] | []// |//] | []// | ].
@@ -1797,6 +1818,9 @@ move: a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(leey, leNye)//.
 by rewrite !lee_fin lerD2l.
 Qed.
 
+Lemma leeD2rE x a b : x \is a fin_num -> (a + x <= b + x) = (a <= b).
+Proof. by rewrite -!(addeC x); exact: leeD2lE. Qed.
+
 Lemma leeD2r x a b : a <= b -> a + x <= b + x.
 Proof. rewrite addeC (addeC b); exact: leeD2l. Qed.
 
@@ -1806,14 +1830,14 @@ move: a b x y => [a| |] [b| |] [x| |] [y| |]; rewrite ?(leey, leNye)//.
 by rewrite !lee_fin; exact: lerD.
 Qed.
 
-Lemma lte_le_add a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.
+Lemma lte_leD a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.
 Proof.
 move: x y a b => [x| |] [y| |] [a| |] [b| |] _ //=; rewrite ?(ltry, ltNyr)//.
 by rewrite !lte_fin; exact: ltr_leD.
 Qed.
 
-Lemma lee_lt_add a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.
-Proof. by move=> afin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed.
+Lemma lee_ltD a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.
+Proof. by move=> afin xa yb; rewrite (addeC a) (addeC x) lte_leD. Qed.
 
 Lemma leeB x y z u : x <= y -> u <= z -> x - z <= y - u.
 Proof.
@@ -1821,7 +1845,7 @@ move: x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=; rewrite ?(leey,leNye)//.
 by rewrite !lee_fin; exact: lerB.
 Qed.
 
-Lemma lte_le_sub z u x y : u \is a fin_num ->
+Lemma lte_leB z u x y : u \is a fin_num ->
   x < z -> u <= y -> x - y < z - u.
 Proof.
 move: z u x y => [z| |] [u| |] [x| |] [y| |] _ //=; rewrite ?(ltry, ltNyr)//.
@@ -2309,8 +2333,6 @@ move=> *; apply: (can_inj oppeK); apply: eq_infty => r.
 by rewrite leeNr -EFinN.
 Qed.
 
-Lemma leeN2 x y : (- x <= - y) = (y <= x). Proof. by rewrite leeNl oppeK. Qed.
-
 Lemma lee_abs x : x <= `|x|.
 Proof. by move: x => [x| |]//=; rewrite lee_fin ler_norm. Qed.
 
@@ -2688,6 +2710,16 @@ Notation lee_subl_addl := leeBlDl (only parsing).
 Notation lee_subr_addr := leeBrDr (only parsing).
 #[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBrDl instead.")]
 Notation lee_subr_addl := leeBrDl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lte_leD` instead.")]
+Notation lte_le_add := lte_leD (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lee_ltD` instead.")]
+Notation lee_lt_add := lee_ltD (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lte_leB` instead.")]
+Notation lte_le_sub := lte_leB (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Use leeN2 instead.")]
+Notation lee_opp2 := leeN2 (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Use lteN2 instead.")]
+Notation lte_opp2 := lteN2 (only parsing).
 
 Module DualAddTheoryRealDomain.
 
@@ -2720,67 +2752,79 @@ Lemma dsube_le0 x y : (x \is a fin_num) || (y \is a fin_num) ->
   (y - x <= 0) = (y <= x).
 Proof. by move=> /orP[?|?]; [rewrite dsuber_le0|rewrite dsubre_le0]. Qed.
 
-Lemma lte_dadd a b x y : a < b -> x < y -> a + x < b + y.
+Lemma lte_dD a b x y : a < b -> x < y -> a + x < b + y.
 Proof. rewrite !dual_addeE lteN2 -lteN2 -(lteN2 y); exact: lteD. Qed.
 
-Lemma lee_daddl x y : 0 <= y -> x <= x + y.
+Lemma lee_dDl x y : 0 <= y -> x <= x + y.
 Proof. rewrite dual_addeE leeNr -oppe_le0; exact: geeDl. Qed.
 
-Lemma lee_daddr x y : 0 <= y -> x <= y + x.
+Lemma lee_dDr x y : 0 <= y -> x <= y + x.
 Proof. rewrite dual_addeE leeNr -oppe_le0; exact: geeDr. Qed.
 
-Lemma gee_daddl x y : y <= 0 -> x + y <= x.
+Lemma gee_dDl x y : y <= 0 -> x + y <= x.
 Proof. rewrite dual_addeE leeNl -oppe_ge0; exact: leeDl. Qed.
 
-Lemma gee_daddr x y : y <= 0 -> y + x <= x.
+Lemma gee_dDr x y : y <= 0 -> y + x <= x.
 Proof. rewrite dual_addeE leeNl -oppe_ge0; exact: leeDr. Qed.
 
-Lemma lte_daddl y x : y \is a fin_num -> (y < y + x) = (0 < x).
+Lemma lte_dDl y x : y \is a fin_num -> (y < y + x) = (0 < x).
 Proof. by rewrite -fin_numN dual_addeE lteNr; exact: gte_subl. Qed.
 
-Lemma lte_daddr y x : y \is a fin_num -> (y < x + y) = (0 < x).
+Lemma lte_dDr y x : y \is a fin_num -> (y < x + y) = (0 < x).
 Proof. by rewrite -fin_numN dual_addeE lteNr addeC; exact: gte_subl. Qed.
 
-Lemma gte_dsubl y x : y \is a fin_num -> (y - x < y) = (0 < x).
+Lemma gte_dBl y x : y \is a fin_num -> (y - x < y) = (0 < x).
 Proof. by rewrite -fin_numN dual_addeE lteNl oppeK; exact: lteDl. Qed.
 
-Lemma gte_dsubr y x : y \is a fin_num -> (- x + y < y) = (0 < x).
+Lemma gte_dBr y x : y \is a fin_num -> (- x + y < y) = (0 < x).
 Proof. by rewrite -fin_numN dual_addeE lteNl oppeK; exact: lteDr. Qed.
 
-Lemma gte_daddl x y : x \is a fin_num -> (x + y < x) = (y < 0).
+Lemma gte_dDl x y : x \is a fin_num -> (x + y < x) = (y < 0).
 Proof.
 by rewrite -fin_numN dual_addeE lteNl -[0]oppe0 lteNr; exact: lteDl.
 Qed.
 
-Lemma gte_daddr x y : x \is a fin_num -> (y + x < x) = (y < 0).
-Proof. by rewrite daddeC; exact: gte_daddl. Qed.
+Lemma gte_dDr x y : x \is a fin_num -> (y + x < x) = (y < 0).
+Proof. by rewrite daddeC; exact: gte_dDl. Qed.
 
-Lemma lte_dadd2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b).
+Lemma lte_dD2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b).
 Proof. by move=> ?; rewrite !dual_addeE lteN2 lteD2lE ?fin_numN// lteN2. Qed.
 
-Lemma lee_dadd2l x a b : a <= b -> x + a <= x + b.
+Lemma lte_dD2rE x a b : x \is a fin_num -> (a + x < b + x) = (a < b).
+Proof.
+move=> ?; rewrite !dual_addeE lteN2 -[RHS]lteN2.
+by rewrite -[RHS](@lteD2rE _ (- x))// fin_numN.
+Qed.
+
+Lemma lee_dD2rE x a b : x \is a fin_num -> (a + x <= b + x) = (a <= b).
+Proof.
+move=> ?; rewrite !dual_addeE leeN2 -[RHS]leeN2.
+by rewrite -[RHS](@leeD2rE _ (- x))// fin_numN.
+Qed.
+
+Lemma lee_dD2l x a b : a <= b -> x + a <= x + b.
 Proof. rewrite !dual_addeE leeN2 -leeN2; exact: leeD2l. Qed.
 
-Lemma lee_dadd2lE x a b : x \is a fin_num -> (x + a <= x + b) = (a <= b).
+Lemma lee_dD2lE x a b : x \is a fin_num -> (x + a <= x + b) = (a <= b).
 Proof. by move=> ?; rewrite !dual_addeE leeN2 leeD2lE ?fin_numN// leeN2. Qed.
 
-Lemma lee_dadd2r x a b : a <= b -> a + x <= b + x.
+Lemma lee_dD2r x a b : a <= b -> a + x <= b + x.
 Proof. rewrite !dual_addeE leeN2 -leeN2; exact: leeD2r. Qed.
 
-Lemma lee_dadd a b x y : a <= b -> x <= y -> a + x <= b + y.
+Lemma lee_dD a b x y : a <= b -> x <= y -> a + x <= b + y.
 Proof. rewrite !dual_addeE leeN2 -leeN2 -(leeN2 y); exact: leeD. Qed.
 
-Lemma lte_le_dadd a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.
-Proof. rewrite !dual_addeE lteN2 -lteN2; exact: lte_le_sub. Qed.
+Lemma lte_le_dD a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.
+Proof. by rewrite !dual_addeE lteN2 -lteN2; exact: lte_leB. Qed.
 
-Lemma lee_lt_dadd a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.
-Proof. by move=> afin xa yb; rewrite (daddeC a) (daddeC x) lte_le_dadd. Qed.
+Lemma lee_lt_dD a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.
+Proof. by move=> afin xa yb; rewrite (daddeC a) (daddeC x) lte_le_dD. Qed.
 
-Lemma lee_dsub x y z t : x <= y -> t <= z -> x - z <= y - t.
+Lemma lee_dB x y z t : x <= y -> t <= z -> x - z <= y - t.
 Proof. rewrite !dual_addeE leeNl oppeK -leeN2 !oppeK; exact: leeD. Qed.
 
-Lemma lte_le_dsub z u x y : u \is a fin_num -> x < z -> u <= y -> x - y < z - u.
-Proof. by rewrite !dual_addeE lteN2 !oppeK -lteN2; exact: lte_le_add. Qed.
+Lemma lte_le_dB z u x y : u \is a fin_num -> x < z -> u <= y -> x - y < z - u.
+Proof. by rewrite !dual_addeE lteN2 !oppeK -lteN2; exact: lte_leD. Qed.
 
 Lemma lee_dsum I (f g : I -> \bar^d R) s (P : pred I) :
   (forall i, P i -> f i <= g i) ->
@@ -2890,16 +2934,16 @@ move=> AB f0; rewrite !dual_sumeE leeN2.
 apply: lee_sum_nneg_subfset => [//|? ? ?]; rewrite oppe_ge0; exact: f0.
 Qed.
 
-Lemma lte_dsubl_addr x y z : y \is a fin_num -> (x - y < z) = (x < z + y).
+Lemma lte_dBlDr x y z : y \is a fin_num -> (x - y < z) = (x < z + y).
 Proof. by move=> ?; rewrite !dual_addeE lteNl lteNr oppeK lteBlDr. Qed.
 
-Lemma lte_dsubl_addl x y z : y \is a fin_num -> (x - y < z) = (x < y + z).
+Lemma lte_dBlDl x y z : y \is a fin_num -> (x - y < z) = (x < y + z).
 Proof. by move=> ?; rewrite !dual_addeE lteNl lteNr lteBrDl ?fin_numN. Qed.
 
-Lemma lte_dsubr_addr x y z : z \is a fin_num -> (x < y - z) = (x + z < y).
+Lemma lte_dBrDr x y z : z \is a fin_num -> (x < y - z) = (x + z < y).
 Proof. by move=> ?; rewrite !dual_addeE lteNl lteNr lteBlDr ?fin_numN. Qed.
 
-Lemma lte_dsubr_addl x y z : z \is a fin_num -> (x < y - z) = (z + x < y).
+Lemma lte_dBrDl x y z : z \is a fin_num -> (x < y - z) = (z + x < y).
 Proof. by move=> ?; rewrite !dual_addeE lteNl lteNr lteBlDl ?fin_numN. Qed.
 
 Lemma lte_dsuber_addr x y z : y \is a fin_num -> (x < y - z) = (x + z < y).
@@ -2955,7 +2999,7 @@ by move=> ?; rewrite !dual_addeE leeNl leeNr lee_subel_addl ?fin_numN.
 Qed.
 
 Lemma dsuber_gt0 x y : x \is a fin_num -> (0 < y - x) = (x < y).
-Proof. by move=> ?; rewrite lte_dsubr_addl// dadde0. Qed.
+Proof. by move=> ?; rewrite lte_dBrDl// dadde0. Qed.
 
 Lemma dsubre_gt0 x y : y \is a fin_num -> (0 < y - x) = (x < y).
 Proof. by move=> ?; rewrite lte_dsuber_addl// dadde0. Qed.
@@ -3029,7 +3073,7 @@ Lemma lee_abs_dsum (I : Type) (s : seq I) (F : I -> \bar^d R) (P : pred I) :
   `|\sum_(i <- s | P i) F i| <= \sum_(i <- s | P i) `|F i|.
 Proof.
 elim/big_ind2 : _ => //; first by rewrite abse0.
-by move=> *; exact/(le_trans (lee_abs_dadd _ _) (lee_dadd _ _)).
+by move=> *; exact/(le_trans (lee_abs_dadd _ _) (lee_dD _ _)).
 Qed.
 
 Lemma lee_abs_dsub x y : `|x - y| <= `|x| + `|y|.
@@ -3047,7 +3091,7 @@ Lemma dmule_natl x n : n%:R%:E * x = x *+ n.
 Proof. by rewrite mule_natl ednatmulE. Qed.
 
 Lemma lee_pdaddl y x z : 0 <= x -> y <= z -> y <= x + z.
-Proof. by move=> *; rewrite -[y]dadd0e lee_dadd. Qed.
+Proof. by move=> *; rewrite -[y]dadd0e lee_dD. Qed.
 
 Lemma lte_pdaddl y x z : 0 <= x -> y < z -> y < x + z.
 Proof. by move=> x0 /lt_le_trans; apply; rewrite lee_pdaddl. Qed.
@@ -3078,21 +3122,56 @@ Arguments lee_dsum_npos_natr {R}.
 Arguments lee_dsum_nneg_natl {R}.
 Arguments lee_dsum_npos_natl {R}.
 
-End DualAddTheoryRealDomain.
-
-Lemma lee_opp2 {R : numDomainType} : {mono @oppe R : x y /~ x <= y}.
-Proof.
-move=> x y; case: x y => [?||] [?||] //; first by rewrite !lee_fin !lerN2.
-  by rewrite  /Order.le/= realN.
-by rewrite /Order.le/= realN.
-Qed.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dD`")]
+Notation lte_dadd := lte_dD (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dDl`")]
+Notation lee_daddl := lee_dDl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dDr`")]
+Notation lee_daddr := lee_dDr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gee_dDl`")]
+Notation gee_daddl := gee_dDl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gee_dDr`")]
+Notation gee_daddr := gee_dDr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dDl`")]
+Notation lte_daddl := lte_dDl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dDr`")]
+Notation lte_daddr := lte_dDr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dBl`")]
+Notation gte_dsubl := gte_dBl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dBr`")]
+Notation gte_dsubr := gte_dBr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dDl`")]
+Notation gte_daddl := gte_dDl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dDr`")]
+Notation gte_daddr := gte_dDr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dD2lE`")]
+Notation lte_dadd2lE := lte_dD2lE (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2rE`")]
+Notation lee_dadd2rE := lee_dD2rE (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2l`")]
+Notation lee_dadd2l := lee_dD2l (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2r`")]
+Notation lee_dadd2r := lee_dD2r (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD`")]
+Notation lee_dadd := lee_dD (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dB`")]
+Notation lee_dsub := lee_dB (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBlDr`")]
+Notation lte_dsubl_addr := lte_dBlDr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBlDl`")]
+Notation lte_dsubl_addl := lte_dBlDl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBrDr`")]
+Notation lte_dsubr_addr := lte_dBrDr (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBrDl`")]
+Notation lte_dsubr_addl := lte_dBrDl (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_le_dD`")]
+Notation lte_le_dadd := lte_le_dD (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_lt_dD`")]
+Notation lee_lt_dadd := lee_lt_dD (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_le_dB`")]
+Notation lte_le_dsub := lte_le_dD (only parsing).
 
-Lemma lte_opp2 {R : numDomainType} : {mono @oppe R : x y /~ x < y}.
-Proof.
-move=> x y; case: x y => [?||] [?||] //; first by rewrite !lte_fin !ltrN2.
-  by rewrite  /Order.lt/= realN.
-by rewrite /Order.lt/= realN.
-Qed.
+End DualAddTheoryRealDomain.
 
 Section realFieldType_lemmas.
 Variable R : realFieldType.
diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v
index 2190aa44c..0f9a8eb96 100644
--- a/theories/lebesgue_measure.v
+++ b/theories/lebesgue_measure.v
@@ -2224,11 +2224,9 @@ move=> V [/[dup] /compact_measurable mV cptV VFND] FDV1 M1FD.
 rewrite (@le_trans _ _ (mu V))//; last first.
   apply: ereal_sup_ub; exists V => //=; split => //.
   exact: (subset_trans VFND (@subIsetr _ _ _)).
-rewrite -(@leeD2lE _ 1)// {1}addeC -EFinD (le_trans M1FD)//.
+rewrite -(@leeD2rE _ 1)// -EFinD (le_trans M1FD)//.
 rewrite /mu (@measureDI _ _ _ _ (F N `&` D) _ _ mV)/=; last exact: measurableI.
-rewrite ltW// lte_le_add // ?ge0_fin_numE //; last first.
-  by rewrite measureIr//; apply: measurableI.
-by rewrite -setIA (le_lt_trans _ (ffin N).2)// measureIl//; exact: measurableI.
+by rewrite addeC leeD//; [rewrite measureIr//; exact: measurableI|exact/ltW].
 Qed.
 
 End lebesgue_regularity.
diff --git a/theories/realfun.v b/theories/realfun.v
index 8a5bdd953..c3e8f3927 100644
--- a/theories/realfun.v
+++ b/theories/realfun.v
@@ -2358,8 +2358,7 @@ rewrite {1}variation_prev; last exact: itv_partition1.
 rewrite /= -addeA -lteBrDr; last by rewrite fin_numD; apply/andP.
 rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA.
 move/lt_trans; apply.
-rewrite [x in (_ < x%:E)%E]splitr EFinD addeC lteD2lE //.
-rewrite -addeA.
+rewrite [in ltRHS](splitr (eps%:num)) EFinD lteD2rE// -addeA.
 apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E).
   rewrite [in leRHS]variation_prev; last exact: itv_partition1.
   rewrite geeDl// sube_le0; apply: ereal_sup_ub => /=.