diff options
| author | herbelin | 2003-12-01 12:19:33 +0000 |
|---|---|---|
| committer | herbelin | 2003-12-01 12:19:33 +0000 |
| commit | 02d962bcf43380c8660846f103c188ae2bd70976 (patch) | |
| tree | 7355bb18f820eb59d18377aa84aa7cd04e72002f | |
| parent | 680494e973b955f120b3568ddf4ff7e9e1f4b37f (diff) | |
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
| -rw-r--r-- | theories/Reals/RIneq.v | 7 |
1 files 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. |