diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6fecd383e..e89889d77 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -39,6 +39,9 @@
 - in `realfun.v`:
   + lemma `nondecreasing_at_left_is_cvgr`
 
+- in `constructive_ereal.v`:
+  + lemmas `lteD2rE`, `leeD2rE`
+
 ### Changed
 
 - in `topology.v`:
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index 831e91b69..3a2b00dc7 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -1783,6 +1783,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 +1800,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.
 
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 => /=.