From 639c724bdd701779ac5a0b94528b6ad95dd25386 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 29 Mar 2024 17:50:37 +0900
Subject: [PATCH 1/2] fixes #1094

---
 CHANGELOG_UNRELEASED.md |  6 ++++++
 theories/exp.v          | 10 ++++++++--
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index e334580f12..cce6e75c24 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -65,6 +65,9 @@
   + definition `notP`
   + hint view for `move/` and `apply/` for `Internals.equivT_LR`, `Internals.equivT_RL`
 
+- in `exp.v`:
+  + lemma `expRMn`
+
 ### Changed
 - moved from `topology.v` to `function_spaces.v`: `prod_topology`, 
     `product_topology_def`, `proj_continuous`, `dfwith_continuous`, 
@@ -143,6 +146,9 @@
   + `SigmaFinite_isFinite` -> `isFinite`
   + `FiniteMeasure_isSubProbability` -> `isSubProbability`
 
+- in `exp.v`:
+  + `expRMm` -> `expRnM`
+
 ### Generalized
 
 - in `realfun.v`
diff --git a/theories/exp.v b/theories/exp.v
index 73a4f32002..6476b68356 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -416,12 +416,15 @@ rewrite expRxDyMexpx expRN [_ * expR y]mulrC mulfK //.
 by case: ltrgt0P (expR_gt0 x).
 Qed.
 
-Lemma expRMm n x : expR (n%:R * x) = expR x ^+ n.
+Lemma expRnM n x : expR (n%:R * x) = expR x ^+ n.
 Proof.
 elim: n x => [x|n IH x] /=; first by rewrite mul0r expr0 expR0.
 by rewrite exprS -nat1r mulrDl mul1r expRD IH.
 Qed.
 
+Lemma expRMn n x : expR (x * n%:R) = expR x ^+ n.
+Proof. by rewrite mulrC expRnM. Qed.
+
 Lemma expR_gt1 x : (1 < expR x) = (0 < x).
 Proof.
 case: ltrgt0P => [x_gt0| xN|->]; last by rewrite expR0.
@@ -506,6 +509,9 @@ Local Close Scope convex_scope.
 
 End expR.
 
+#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `expRnM`")]
+Notation expRMm := expRnM (only parsing).
+
 Section expeR.
 Context {R : realType}.
 Implicit Types (x y : \bar R) (r s : R).
@@ -895,7 +901,7 @@ rewrite le_eqVlt => /predU1P[<-|a0].
   by rewrite powR0 ?invr_eq0 ?pnatr_eq0// sqrtr0.
 have /eqP : (a `^ (2^-1)) ^+ 2 = (Num.sqrt a) ^+ 2.
   rewrite sqr_sqrtr; last exact: ltW.
-  by rewrite /powR gt_eqF// -expRMm mulrA divrr ?mul1r ?unitfE// lnK.
+  by rewrite /powR gt_eqF// -expRnM mulrA divrr ?mul1r ?unitfE// lnK.
 rewrite eqf_sqr => /predU1P[//|/eqP h].
 have : 0 < a `^ 2^-1 by exact: powR_gt0.
 by rewrite h oppr_gt0 ltNge sqrtr_ge0.

From e528752e85d2356be0f49f4d2e500091ddb9ca81 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Sun, 31 Mar 2024 15:12:03 +0900
Subject: [PATCH 2/2] more conservative version

---
 CHANGELOG_UNRELEASED.md |  4 ++--
 theories/exp.v          | 12 ++++++------
 2 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index cce6e75c24..e67d620275 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -66,7 +66,7 @@
   + hint view for `move/` and `apply/` for `Internals.equivT_LR`, `Internals.equivT_RL`
 
 - in `exp.v`:
-  + lemma `expRMn`
+  + lemma `expRM_natr`
 
 ### Changed
 - moved from `topology.v` to `function_spaces.v`: `prod_topology`, 
@@ -147,7 +147,7 @@
   + `FiniteMeasure_isSubProbability` -> `isSubProbability`
 
 - in `exp.v`:
-  + `expRMm` -> `expRnM`
+  + `expRMm` -> `expRM_natl`
 
 ### Generalized
 
diff --git a/theories/exp.v b/theories/exp.v
index 6476b68356..de5bbfc1c3 100644
--- a/theories/exp.v
+++ b/theories/exp.v
@@ -416,14 +416,14 @@ rewrite expRxDyMexpx expRN [_ * expR y]mulrC mulfK //.
 by case: ltrgt0P (expR_gt0 x).
 Qed.
 
-Lemma expRnM n x : expR (n%:R * x) = expR x ^+ n.
+Lemma expRM_natl n x : expR (n%:R * x) = expR x ^+ n.
 Proof.
 elim: n x => [x|n IH x] /=; first by rewrite mul0r expr0 expR0.
 by rewrite exprS -nat1r mulrDl mul1r expRD IH.
 Qed.
 
-Lemma expRMn n x : expR (x * n%:R) = expR x ^+ n.
-Proof. by rewrite mulrC expRnM. Qed.
+Lemma expRM_natr n x : expR (x * n%:R) = expR x ^+ n.
+Proof. by rewrite mulrC expRM_natl. Qed.
 
 Lemma expR_gt1 x : (1 < expR x) = (0 < x).
 Proof.
@@ -509,8 +509,8 @@ Local Close Scope convex_scope.
 
 End expR.
 
-#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `expRnM`")]
-Notation expRMm := expRnM (only parsing).
+#[deprecated(since="mathcomp-analysis 1.1.0", note="renamed `expRM_natl`")]
+Notation expRMm := expRM_natl (only parsing).
 
 Section expeR.
 Context {R : realType}.
@@ -901,7 +901,7 @@ rewrite le_eqVlt => /predU1P[<-|a0].
   by rewrite powR0 ?invr_eq0 ?pnatr_eq0// sqrtr0.
 have /eqP : (a `^ (2^-1)) ^+ 2 = (Num.sqrt a) ^+ 2.
   rewrite sqr_sqrtr; last exact: ltW.
-  by rewrite /powR gt_eqF// -expRnM mulrA divrr ?mul1r ?unitfE// lnK.
+  by rewrite /powR gt_eqF// -expRM_natl mulrA divrr ?mul1r ?unitfE// lnK.
 rewrite eqf_sqr => /predU1P[//|/eqP h].
 have : 0 < a `^ 2^-1 by exact: powR_gt0.
 by rewrite h oppr_gt0 ltNge sqrtr_ge0.