From 02d962bcf43380c8660846f103c188ae2bd70976 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 1 Dec 2003 12:19:33 +0000
Subject: Ratage standardisation Rge_monotony en Rmult_ge_compat_r

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5047 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/RIneq.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 5534cde45c..ad67223ad4 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1077,9 +1077,8 @@ Qed.
 
 (***********)
 Lemma Rmult_ge_compat_r :
- forall r r1 r2, r2 >= 0 -> r >= r1 -> r * r2 >= r1 * r2.
-intros x y z; intros; apply Rle_ge; apply Rmult_le_compat_r; apply Rge_le;
- assumption.
+ forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r.
+intros; apply Rle_ge; apply Rmult_le_compat_r; apply Rge_le; assumption.
 Qed.
 
 (***********)
@@ -1629,4 +1628,4 @@ Lemma completeness_weak :
  forall E:R -> Prop,
    bound E -> ( exists x : R | E x) ->  exists m : R | is_lub E m.
 intros; elim (completeness E H H0); intros; split with x; assumption.
-Qed.
\ No newline at end of file
+Qed.
-- 
cgit v1.2.3