diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 4eb9b73b1a..3d16ebda51 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -49,6 +49,10 @@
 - in `lebesgue_integral.v`:
   + notations `\x`, `\x^` for `product_measure1` and `product_measure2`
 
+- in `constructive_ereal.v`:
+  + lemmas `expeS`, `fin_numX`
+
+
 ### Changed
 
 - in `fsbigop.v`:
diff --git a/theories/constructive_ereal.v b/theories/constructive_ereal.v
index a4cddb5d6d..a16b90f6ec 100644
--- a/theories/constructive_ereal.v
+++ b/theories/constructive_ereal.v
@@ -717,6 +717,9 @@ Proof. by move: x => [r| |]/=; rewrite /mule/= ?mul0r// eqxx. Qed.
 
 Canonical mule_mulmonoid := @Monoid.MulLaw _ _ mule mul0e mule0.
 
+Lemma expeS x n : x ^+ n.+1 = x * x ^+ n.
+Proof. by case: n => //=; rewrite mule1. Qed.
+
 Definition mule_def x y :=
   ~~ (((x == 0) && (`| y | == +oo)) || ((y == 0) && (`| x | == +oo))).
 
@@ -814,6 +817,9 @@ Lemma fin_numM x y : x \is a fin_num -> y \is a fin_num ->
   x * y \is a fin_num.
 Proof. by move: x y => [x| |] [y| |]. Qed.
 
+Lemma fin_numX x n : x \is a fin_num -> x ^+ n \is a fin_num.
+Proof. by elim: n x => // n ih x finx; rewrite expeS fin_numM// ih. Qed.
+
 Lemma fineD : {in @fin_num R &, {morph fine : x y / x + y >-> (x + y)%R}}.
 Proof. by move=> [r| |] [s| |]. Qed.