diff options
author | 2003-11-02 00:02:31 +0000 | |
---|---|---|
committer | 2003-11-02 00:02:31 +0000 | |
commit | 94f386e3b5558a16799d844128f1a5ab29560c58 (patch) | |
tree | c867e6a28f1f177f14b0418d7b5275b622835e4a | |
parent | d030c8f18316d63c1d9bda68448ccc70187694f6 (diff) |
Restauration preference Rge a Rle pour compatibilite...; petit nettoyage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4768 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/Reals/RIneq.v | 38 |
1 files changed, 15 insertions, 23 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index cddc1a541..9d877840c 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -109,19 +109,21 @@ Lemma Rle_ge : (r1,r2:R)``r1<=r2`` -> ``r2>=r1``. NewDestruct 1; Red; Auto with real. Qed. -Hints Resolve Rle_ge : real. +Hints Immediate Rle_ge : real. (**********) Lemma Rge_le : (r1,r2:R)``r1>=r2`` -> ``r2<=r1``. NewDestruct 1; Red; Auto with real. Qed. +Hints Resolve Rge_le : real. + (**********) Lemma not_Rle:(r1,r2:R)~``r1<=r2`` -> ``r2<r1``. Intros r1 r2 ; Generalize (total_order r1 r2) ; Unfold Rle; Tauto. Qed. -Hints Immediate Rge_le not_Rle : real. +Hints Immediate not_Rle : real. Lemma not_Rge:(r1,r2:R)~``r1>=r2`` -> ``r1<r2``. Intros; Apply not_Rle; Auto with real. @@ -726,7 +728,6 @@ Hints Immediate Ropp_Rle : real. Lemma Rle_Ropp1:(r1,r2:R) ``r2 <= r1`` -> ``-r1 <= -r2``. Intros r1 r2 H;Elim H;Auto with real. -Intro H1;Rewrite H1;Auto with real. Qed. Hints Resolve Rle_Ropp1 : real. @@ -777,6 +778,10 @@ Generalize (Rlt_monotony z y x H Eq0);Intro;ElimType False; Apply (Rlt_antirefl ``z*x``);Auto. Qed. +V7only [ +Notation Rlt_monotony_rev := [r,r1,r2:R](Rlt_monotony_contra r1 r2 r). +]. + Lemma Rlt_anti_monotony:(r,r1,r2:R)``r < 0`` -> ``r1 < r2`` -> ``r*r1 > r*r2``. Intros; Replace r with ``-(-r)``; Auto with real. Rewrite (Ropp_mul1 ``-r``); Rewrite (Ropp_mul1 ``-r``). @@ -820,7 +825,7 @@ Hints Resolve Rle_anti_monotony1 : real. Lemma Rle_anti_monotony :(r,r1,r2:R)``r <= 0`` -> ``r1 <= r2`` -> ``r*r1 >= r*r2``. -Auto with real. +Intros; Apply Rle_ge; Auto with real. Qed. Hints Resolve Rle_anti_monotony : real. @@ -840,6 +845,12 @@ Lemma Rmult_lt:(r1,r2,r3,r4:R)``r3>0`` -> ``r2>0`` -> Intros; Apply Rlt_trans with ``r2*r3``; Auto with real. Qed. +(*********) +Lemma Rmult_lt_0 + :(r1,r2,r3,r4:R)``r3>=0``->``r2>0``->``r1<r2``->``r3<r4``->``r1*r3<r2*r4``. +Intros; Apply Rle_lt_trans with ``r2*r3``; Auto with real. +Qed. + (** Order and Substractions *) Lemma Rlt_minus:(r1,r2:R)``r1 < r2`` -> ``r1-r2 < 0``. Intros; Apply (Rlt_anti_compatibility ``r2``). @@ -922,17 +933,6 @@ Replace ``0`` with ``r*0``; Auto with real. Qed. Hints Resolve Rlt_Rinv2 : real. -(**********) -Lemma Rlt_monotony_rev: - (r,r1,r2:R)``0<r`` -> ``r*r1 < r*r2`` -> ``r1 < r2``. -Intros; Replace r1 with ``/r*(r*r1)``. -Replace r2 with ``/r*(r*r2)``; Auto with real. -Transitivity ``r*/r*r2``; Auto with real. -Ring. -Transitivity ``r*/r*r1``; Auto with real. -Ring. -Qed. - (*********) Lemma Rinv_lt:(r1,r2:R)``0 < r1*r2`` -> ``r1 < r2`` -> ``/r2 < /r1``. Intros; Apply Rlt_monotony_rev with ``r1*r2``; Auto with real. @@ -997,11 +997,9 @@ Qed. Lemma Rle_sym1:(r1,r2:R)``r1<=r2``->``r2>=r1``. Proof Rle_ge. -V7only [ Notation "'Rle_sym2' a b c" := (Rge_le b a c) (at level 10, a,b,c at level 9, only parsing). Notation Rle_sym2 := Rge_le (only parsing). -]. (* (**********) Lemma Rle_sym2:(r1,r2:R)``r2>=r1`` -> ``r1<=r2``. @@ -1128,12 +1126,6 @@ Replace ``0`` with ``0*r2``; Auto with real. Qed. (*********) -Lemma Rmult_lt_0 - :(r1,r2,r3,r4:R)``r3>=0``->``r2>0``->``r1<r2``->``r3<r4``->``r1*r3<r2*r4``. -Intros; Apply Rle_lt_trans with ``r2*r3``; Auto with real. -Qed. - -(*********) Lemma Rmult_lt_pos:(x,y:R)``0<x`` -> ``0<y`` -> ``0<x*y``. Proof Rmult_gt. |