Merge pull request #213 from damiendoligez/fix-rmult-gt-reg-l

Fix statement of Rmult_gt_reg_l in RIneq.v

Author: proux01

doc/changelog/01-changed/213-fix-rmult-gt-reg-l.rst

@@ -0,0 +1,8 @@
+- in `RIneq.v`
+
+  + Changed the statement of `Rmult_gt_reg_l`.
+    Use the convertible `Rmult_lt_reg_l`
+    if you need a backward compatible solution
+    (`#213 <https://github.com/coq/stdlib/pull/213>`_,
+    fixes `#212 <https://github.com/coq/stdlib/issues/212>`_,
+    by Damien Doligez).

theories/Reals/RIneq.v

@@ -1662,7 +1662,7 @@ Proof.
   now rewrite 2(Rmult_comm r).
 Qed.
 
-Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
+Lemma Rmult_gt_reg_l : forall r r1 r2, r > 0 -> r * r1 > r * r2 -> r1 > r2.
 Proof. now intros r r1 r2; apply Rmult_lt_reg_l. Qed.
 
 Lemma Rmult_gt_reg_r : forall r r1 r2, r > 0 -> r1 * r > r2 * r -> r1 > r2.