diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 60c4e915b..04da26dd2 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -13,6 +13,9 @@
 - in `num_normedtype.v`:
   + lemma `nbhs_infty_gtr`
 
+- in `constructive_ereal.v`:
+  + lemma `lt0_adde`
+
 ### Changed
 
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index f48e46ca7..97fb2eaa2 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -1743,6 +1743,17 @@ Qed.
 Lemma lte_add_pinfty x y : x < +oo -> y < +oo -> x + y < +oo.
 Proof. by move: x y => -[r [r'| |]| |] // ? ?; rewrite -EFinD ltry. Qed.
 
+Lemma lt0_adde x y : x + y < 0 -> (x < 0) || (y < 0).
+Proof.
+move: x y => [x| |] [y| |]//; rewrite ?lee_fin ?lte_fin.
+- rewrite !ltNge -negb_and; apply: contra.
+  by move=> /andP[? ?]; rewrite addr_ge0.
+- by move=> _; rewrite ltNyr orbT.
+- by move=> _; rewrite ltNyr.
+- by move=> _; rewrite ltNy0.
+- by rewrite ltNy0.
+Qed.
+
 Lemma lte_sum_pinfty I (s : seq I) (P : pred I) (f : I -> \bar R) :
   (forall i, P i -> f i < +oo) -> \sum_(i <- s | P i) f i < +oo.
 Proof.