diff options
Diffstat (limited to 'theories')
| -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. |