fixes #1094 (renaming of expRMm) (#1200)

* fixes #1094

* more conservative version

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 `expRM_natr`
+
 ### 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` -> `expRM_natl`
+
 ### Generalized
 
 - in `realfun.v`

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 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 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.
 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 `expRM_natl`")]
+Notation expRMm := expRM_natl (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// -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.