From e2461a701cbda7580763f478988d9946b5dddb9a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 16 Oct 2003 14:31:27 +0000
Subject: Ajout de quelques lemmes cles

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

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.
-- 
cgit v1.2.3