diff options
| author | herbelin | 2003-10-16 14:31:27 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-16 14:31:27 +0000 |
| commit | e2461a701cbda7580763f478988d9946b5dddb9a (patch) | |
| tree | 59a566be12b9290ad3467c8d7c7edcef0b87baad | |
| parent | 2d55be3f00e6fbc4ff91c4d3138dca2d68db587b (diff) | |
Ajout de quelques lemmes cles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4645 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Reals/RIneq.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 78c4a5edc9..250ab423b7 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -56,6 +56,10 @@ Lemma Rlt_antirefl:(r:R)~``r<r``. Qed. Hints Resolve Rlt_antirefl : real. +Lemma Rle_refl : (x:R) ``x<=x``. +Intro; Right; Reflexivity. +Qed. + Lemma Rlt_not_eq:(r1,r2:R)``r1<r2``->``r1<>r2``. Red; Intros r1 r2 H H0; Apply (Rlt_antirefl r1). Pattern 2 r1; Rewrite H0; Trivial. @@ -119,6 +123,10 @@ Qed. Hints Immediate Rge_le not_Rle : real. +Lemma not_Rge:(r1,r2:R)~``r1>=r2`` -> ``r1<r2``. +Intros; Apply not_Rle; Auto with real. +Qed. + (**********) Lemma Rlt_le_not:(r1,r2:R)``r2<r1`` -> ~``r1<=r2``. Generalize Rlt_antisym imp_not_Req ; Unfold Rle. @@ -891,6 +899,11 @@ Unfold Rsqr; Auto with real. Qed. Hints Resolve Rlt_R0_R1 : real. +Lemma Rle_R0_R1:``0<=1``. +Left. +Exact Rlt_R0_R1. +Qed. + (** Order and inverse *) Lemma Rlt_Rinv:(r:R)``0<r``->``0</r``. Intros; Apply not_Rle; Red; Intros. |