minor generalization (#1504)

Co-authored-by: Alessandro Bruni <brun@itu.dk>
math-comp · Feb 27, 2025 · b1f05da · b1f05da
1 parent b709261
commit b1f05da
Show file tree

Hide file tree

Showing 2 changed files with 5 additions and 2 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -27,6 +27,9 @@
 
 ### Generalized
 
+- in `constructive_ereal.v`:
+  + lemma `EFin_natmul`
+
 ### Deprecated
 
 ### Removed

diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
@@ -707,8 +707,8 @@ Proof. by elim: n => //= n ->. Qed.
 Lemma enatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.
 Proof. by elim: n => //= n ->. Qed.
 
-Lemma EFin_natmul (r : R) n : (r *+ n.+1)%:E = r%:E *+ n.+1.
-Proof. by elim: n => //= n <-. Qed.
+Lemma EFin_natmul (r : R) n : (r *+ n)%:E = r%:E *+ n.
+Proof. by case: n => //; elim => //= n <-. Qed.
 
 Lemma mule2n x : x *+ 2 = x + x. Proof. by []. Qed.