diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 6638a5a47a..3025d70f92 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -56,6 +56,8 @@
   + lemmas `ereal_supP`, `ereal_infP`, `ereal_sup_gtP`, `ereal_inf_ltP`,
     `ereal_inf_leP`, `ereal_sup_geP`, `lb_ereal_infNy_adherent`,
     `ereal_sup_real`, `ereal_inf_real`
+- in `constructive_ereal.v`:
+  + lemmas `expe_ge0`, `expe_eq0`, `expe_gt0`
 
 ### Changed
 
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index 560f65caed..511405b036 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -1394,6 +1394,15 @@ Qed.
 Lemma lte0_abs x : x < 0 -> `|x| = - x.
 Proof. by move=> /ltW/lee0_abs. Qed.
 
+Lemma expe_eq0 x n : (x ^+ n == 0) = (n > 0)%N && (x == 0).
+Proof. by elim: n => [|n ih]; rewrite ?expeS ?mule_eq0 ?ih ?andKb// gt_eqF. Qed.
+
+Lemma expe_gt0 x n : 0 < x -> 0 < x ^+ n.
+Proof. by elim: n => //n ih /[dup] /ih xn0 x0; rewrite expeS mule_gt0. Qed.
+
+Lemma expe_ge0 x n : 0 <= x -> 0 <= x ^+ n.
+Proof. by elim: n => // n ih x0; rewrite expeS mule_ge0// ih. Qed.
+
 End ERealArithTh_numDomainType.
 Notation "x +? y" := (adde_def x%dE y%dE) : ereal_dual_scope.
 Notation "x +? y" := (adde_def x y) : ereal_scope.