Nouvelle interprétation des nombres réels

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3499 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 16 insertions, 13 deletions

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 828962656..494a7d685 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -39,17 +39,20 @@ Tactic Definition DiscrR :=
         Replace ?1 with (INR nbr);
           [Apply not_O_INR;Discriminate|Simpl;Ring]).
 
-Tactic Definition Sup0_lt trm:=
-  Replace ``0`` with (INR O);
-  [Let nbr=(ToINR trm) In
-      Replace trm with (INR nbr);
-      [Apply lt_INR; Apply lt_O_Sn|Simpl;Ring]|Simpl;Reflexivity].
-
-Tactic Definition Sup0_gt trm:=
-  Unfold Rgt; Sup0_lt trm.   
-
-Tactic Definition Sup0 :=
+Lemma Rlt_R0_R2 : ``0<2``.
+Replace ``2`` with (INR (2)); [Apply lt_INR_0; Apply lt_O_Sn | Reflexivity].
+Qed.
+
+Lemma Rplus_lt_pos : (x,y:R) ``0<x`` -> ``0<y`` -> ``0<x+y``.
+Intros.
+Apply Rlt_trans with x.
+Assumption. 
+Pattern 1 x; Rewrite <- Rplus_Or.
+Apply Rlt_compatibility.
+Assumption.
+Qed.
+
+Recursive Tactic Definition Sup0 :=
   Match Context With
-  | [ |- ``0<?1`` ] -> (Sup0_lt ?1)
-  | [ |- ``?1>0`` ] -> (Sup0_gt ?1).
-
+  | [ |- ``0<?1`` ] -> Repeat (Apply Rmult_lt_pos Orelse Apply Rplus_lt_pos; Try Apply Rlt_R0_R1 Orelse Apply Rlt_R0_R2)
+  | [ |- ``?1>0`` ] -> Change ``0<?1``; Sup0.
\ No newline at end of file