Ajout d'une syntaxe pour Reals.

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

6 files changed, 402 insertions, 565 deletions

diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 2297e7d7b..21ab28be8 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -7,31 +7,9 @@
 (*********************************************************)
 
 Require Export ZArith.
+Require Export Rsyntax.
 Require Export TypeSyntax.
 
-Parameter R:Type.
-Parameter R0:R.
-Parameter R1:R.
-Parameter Rplus:R->R->R.
-Parameter Rmult:R->R->R.
-Parameter Ropp:R->R.
-Parameter Rinv:R->R. 
-Parameter Rlt:R->R->Prop.    
-Parameter up:R->Z.
-(*********************************************************)
-
-(**********)
-Definition Rgt:R->R->Prop:=[r1,r2:R](Rlt r2 r1).
-
-(**********)
-Definition Rle:R->R->Prop:=[r1,r2:R]((Rlt r1 r2)\/(r1==r2)).
-
-(**********)
-Definition Rge:R->R->Prop:=[r1,r2:R]((Rgt r1 r2)\/(r1==r2)).
-
-(**********)
-Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
-
 (*********************************************************)
 (*       Field axioms                                   *)
 (*********************************************************)
@@ -40,18 +18,17 @@ Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
 (*********************************************************)
 
 (**********)
-Axiom Rplus_sym:(r1,r2:R)((Rplus r1 r2)==(Rplus r2 r1)).
+Axiom Rplus_sym:(r1,r2:R)``r1+r2==r2+r1``.
 
 (**********)
-Axiom Rplus_assoc:(r1,r2,r3:R)
-  ((Rplus (Rplus r1 r2) r3)==(Rplus r1 (Rplus r2 r3))).
+Axiom Rplus_assoc:(r1,r2,r3:R)``(r1+r2)+r3==r1+(r2+r3)``.
 
 (**********)
-Axiom Rplus_Ropp_r:(r:R)((Rplus r (Ropp r))==R0).
+Axiom Rplus_Ropp_r:(r:R)``r+(-r)==0``.
 Hints Resolve Rplus_Ropp_r : real v62.
 
 (**********)
-Axiom Rplus_ne:(r:R)(((Rplus r R0)==r)/\((Rplus R0 r)==r)).
+Axiom Rplus_ne:(r:R)``r+0==r``/\``0+r==r``.
 Hints Resolve Rplus_ne : real v62.
 
 (***********************************************************)       
@@ -59,19 +36,18 @@ Hints Resolve Rplus_ne : real v62.
 (***********************************************************)
 
 (**********)
-Axiom Rmult_sym:(r1,r2:R)((Rmult r1 r2)==(Rmult r2 r1)).
+Axiom Rmult_sym:(r1,r2:R)``r1*r2==r2*r1``.
 Hints Resolve Rmult_sym : real v62. 
 
 (**********)
-Axiom Rmult_assoc:(r1,r2,r3:R)
-  ((Rmult (Rmult r1 r2) r3)==(Rmult r1 (Rmult r2 r3))).
+Axiom Rmult_assoc:(r1,r2,r3:R)``(r1*r2)*r3==r1*(r2*r3)``.
 Hints Resolve Rmult_assoc : real v62.
 
 (**********)
-Axiom Rinv_l:(r:R)(~(r==R0))->((Rmult (Rinv r) r)==R1).
+Axiom Rinv_l:(r:R)``r<>0``->``(1/r)*r==1``.
 
 (**********)
-Axiom Rmult_ne:(r:R)(((Rmult r R1)==r)/\((Rmult R1 r)==r)).
+Axiom Rmult_ne:(r:R)``r*1==r``/\``1*r==r``.
 Hints Resolve Rmult_ne : real v62.
 
 (**********)
@@ -82,8 +58,7 @@ Axiom R1_neq_R0:(~R1==R0).
 (*********************************************************)
 
 (**********)
-Axiom Rmult_Rplus_distr:(r1,r2,r3:R)
-  ((Rmult r1 (Rplus r2 r3))==(Rplus (Rmult r1 r2) (Rmult r1 r3))).
+Axiom Rmult_Rplus_distr:(r1,r2,r3:R)``r1*(r2+r3)==(r1*r2)+(r1*r3)``.
 Hints Resolve Rmult_Rplus_distr : real v62.
 
 (*********************************************************)
@@ -94,27 +69,24 @@ Hints Resolve Rmult_Rplus_distr : real v62.
 (*********************************************************)
 
 (**********)
-Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT (Rlt r1 r2) (r1==r2)) 
-                                   (Rgt r1 r2)).
+Axiom total_order_T:(r1,r2:R)(sumorT (sumboolT ``r1<r2`` r1==r2) ``r1>r2``).
 
 (*********************************************************)
 (*       Lower                                           *)
 (*********************************************************)
 
 (**********)
-Axiom Rlt_antisym:(r1,r2:R)(Rlt r1 r2) -> ~(Rlt r2 r1).
+Axiom Rlt_antisym:(r1,r2:R)``r1<r2`` -> ~ ``r2<r1``.
 
 (**********)
 Axiom Rlt_trans:(r1,r2,r3:R)
-  (Rlt r1 r2)->(Rlt r2 r3)->(Rlt r1 r3).
+  ``r1<r2``->``r2<r3``->``r1<r3``.
 
 (**********)
-Axiom Rlt_compatibility:(r,r1,r2:R)(Rlt r1 r2)->
-      (Rlt (Rplus r r1) (Rplus r r2)).
+Axiom Rlt_compatibility:(r,r1,r2:R)``r1<r2``->``r+r1<r+r2``.
 
 (**********)
-Axiom Rlt_monotony:(r,r1,r2:R)(Rlt R0 r)->(Rlt r1 r2)->
-      (Rlt (Rmult r r1) (Rmult r r2)).
+Axiom Rlt_monotony:(r,r1,r2:R)``0<r``->``r1<r2``->``r*r1<r*r2``.
 
 (**********************************************************) 
 (*       Injection from N to R                            *)
@@ -143,22 +115,21 @@ Definition IZR:Z->R:=[z:Z](Cases z of
 (**********************************************************)
 
 (**********)
-Axiom archimed:(r:R)(Rgt (IZR (up r)) r)/\
-                    (Rle (Rminus (IZR (up r)) r) R1).
+Axiom archimed:(r:R)``(IZR (up r)) > r``/\``(IZR (up r))-r <= 1``.
 
 (**********************************************************)
 (*       R Complete                                        *)
 (**********************************************************)
 
 (**********)
-Definition is_upper_bound:=[E:R->Prop][m:R](x:R)(E x)->(Rle x m).
+Definition is_upper_bound:=[E:R->Prop][m:R](x:R)(E x)->``x <= m``.
 
 (**********)
 Definition bound:=[E:R->Prop](ExT [m:R](is_upper_bound E m)).
 
 (**********)
 Definition is_lub:=[E:R->Prop][m:R]
-    (is_upper_bound E m)/\(b:R)(is_upper_bound E b)->(Rle m b).
+    (is_upper_bound E m)/\(b:R)(is_upper_bound E b)->``m <= b``.
 
 (**********)
 Axiom complet:(E:R->Prop)(bound E)->
diff --git a/theories/Reals/Rbase.v b/theories/Reals/Rbase.v
index b459a3d85..970b18ee4 100644
--- a/theories/Reals/Rbase.v
+++ b/theories/Reals/Rbase.v
@@ -45,7 +45,7 @@ Save.
 Hints Resolve Req_EM : real v62.
 
 (**********)
-Lemma total_order:(r1,r2:R)((Rlt r1 r2)\/(r1==r2)\/(Rgt r1 r2)).
+Lemma total_order:(r1,r2:R)``r1<r2``\/(r1==r2)\/``r1>r2``.
 Intros;Elim (total_order_T r1 r2);Intro;Auto.
 Elim y;Intro;Auto.
 Save.
@@ -606,6 +606,15 @@ Intros; Generalize (Rlt_compatibility r3 r1 r2 H);
 Save.
 
 (*********)
+Lemma Rplus_lt_le_lt:(r1,r2,r3,r4:R)(Rlt r1 r2)->(Rle r3 r4)->
+ (Rlt (Rplus r1 r3) (Rplus r2 r4)).
+Intros;Unfold Rle in H0; Elim H0.
+Exact (Rplus_lt r1 r2 r3 r4 H).
+Intro;Rewrite H1;Rewrite (Rplus_sym r1 r4);Rewrite (Rplus_sym r2 r4);
+ Exact (Rlt_compatibility r4 r1 r2 H).
+Save.
+
+(*********)
 Lemma Rmult_lt:(r1,r2,r3,r4:R)(Rgt r3 R0)->(Rgt r2 R0)->
   (Rlt r1 r2)->(Rlt r3 r4)->(Rlt (Rmult r1 r3) (Rmult r2 r4)).
 Intros;Unfold Rgt in H H0;Generalize (Rlt_monotony r3 r1 r2 H H1);Intro;
@@ -951,6 +960,19 @@ Unfold Rgt;Intros;Generalize (Rlt_monotony r1 R0 r2 H H0);Intro;
 Save.
 
 (*********)
+Lemma Rmult_lt_0:(r1,r2,r3,r4:R)(Rge r3 R0)->(Rgt r2 R0)->
+  (Rlt r1 r2)->(Rlt r3 r4)->(Rlt (Rmult r1 r3) (Rmult r2 r4)).
+Intros;Elim H.
+Intro;Exact (Rmult_lt r1 r2 r3 r4 H3 H0 H1 H2).
+Intro;Rewrite H3;Rewrite (Rmult_Or r1);
+ Cut (Rgt r4 R0).
+Intro;Exact (Rmult_gt r2 r4 H0 H4).
+Cut (Rle R0 r3).
+Intro;Exact (Rle_lt_trans R0 r3 r4 H4 H2).
+Exact (Rle_sym2 R0 r3 H).
+Save.
+
+(*********)
 Lemma Rmult_lt_pos:(x,y:R)(Rlt R0 x)->(Rlt R0 y)->(Rlt R0 (Rmult x y)).
 Generalize Rmult_gt;Unfold Rgt;Auto.
 Save.
diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v
new file mode 100644
index 000000000..ecaa7b4ca
--- /dev/null
+++ b/theories/Reals/Rdefinitions.v
@@ -0,0 +1,36 @@
+(* $Id$ *)
+
+
+(*********************************************************)
+(*           Definitions for the axiomatization          *)
+(*                                                       *)
+(*********************************************************)
+
+Require Export ZArith.
+Require Export TypeSyntax.
+
+Parameter R:Type.
+Parameter R0:R.
+Parameter R1:R.
+Parameter Rplus:R->R->R.
+Parameter Rmult:R->R->R.
+Parameter Ropp:R->R.
+Parameter Rinv:R->R. 
+Parameter Rlt:R->R->Prop.    
+Parameter up:R->Z.
+(*********************************************************)
+
+(**********)
+Definition Rgt:R->R->Prop:=[r1,r2:R](Rlt r2 r1).
+
+(**********)
+Definition Rle:R->R->Prop:=[r1,r2:R]((Rlt r1 r2)\/(r1==r2)).
+
+(**********)
+Definition Rge:R->R->Prop:=[r1,r2:R]((Rgt r1 r2)\/(r1==r2)).
+
+(**********)
+Definition Rminus:R->R->R:=[r1,r2:R](Rplus r1 (Ropp r2)).
+
+(**********)
+Definition Rdiv:R->R->R:=[r1,r2:R](Rmult r1 (Rinv r2)).
diff --git a/theories/Reals/Reals.v b/theories/Reals/Reals.v
index c9ee14137..3af2faa4c 100644
--- a/theories/Reals/Reals.v
+++ b/theories/Reals/Reals.v
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+Require Export Rdefinitions.
 Require Export TypeSyntax.
 Require Export Raxioms.
 Require Export Rbase.
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 56a7c709d..465dfd7a4 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -134,6 +134,53 @@ Clear H0;Generalize (H r H1); Intro;Generalize (Rlt_antirefl r);
  Intro;ElimType False; Auto.
 Save.
 
+(*********)
+Definition mul_factor := [l,l':R](Rinv (Rplus R1 (Rplus (Rabsolu l) 
+                                                        (Rabsolu l')))).
+
+(*********)
+Lemma mul_factor_wd : (l,l':R)
+  ~(Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))==R0.
+Intros;Rewrite (Rplus_sym R1 (Rplus (Rabsolu l) (Rabsolu l')));
+ Apply tech_Rplus.
+Cut (Rle (Rabsolu (Rplus l l')) (Rplus (Rabsolu l) (Rabsolu l'))).
+Cut (Rle R0 (Rabsolu (Rplus l l'))).
+Exact (Rle_trans ? ? ?).
+Exact (Rabsolu_pos (Rplus l l')).
+Exact (Rabsolu_triang ? ?).
+Exact Rlt_R0_R1.
+Save.
+
+(*********)
+Lemma mul_factor_gt:(eps:R)(l,l':R)(Rgt eps R0)->
+      (Rgt (Rmult eps (mul_factor l l')) R0).
+Intros;Unfold Rgt;Rewrite <- (Rmult_Or eps);Apply Rlt_monotony.
+Assumption.
+Unfold mul_factor;Apply Rlt_Rinv;
+ Cut (Rle R1 (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))).
+Cut (Rlt R0 R1).
+Exact (Rlt_le_trans ? ? ?).
+Exact Rlt_R0_R1.
+Replace (Rle R1 (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l'))))
+ with (Rle (Rplus R1 R0) (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l')))).
+Apply Rle_compatibility.
+Cut (Rle (Rabsolu (Rplus l l')) (Rplus (Rabsolu l) (Rabsolu l'))).
+Cut (Rle R0 (Rabsolu (Rplus l l'))).
+Exact (Rle_trans ? ? ?).
+Exact (Rabsolu_pos ?).
+Exact (Rabsolu_triang ? ?).
+Rewrite (proj1 ? ? (Rplus_ne R1));Trivial.
+Save.
+
+(*********)
+Lemma mul_factor_gt_f:(eps:R)(l,l':R)(Rgt eps R0)->
+      (Rgt (Rmin R1 (Rmult eps (mul_factor l l'))) R0).
+Intros;Apply Rmin_Rgt_r;Split.
+Exact Rlt_R0_R1.
+Exact (mul_factor_gt eps l l' H).
+Save.
+
+
 (*******************************)
 (*      Metric space           *)
 (*******************************)
@@ -329,6 +376,16 @@ Unfold 2 3 Rminus;
  Apply (eq_Rle (Rminus x y) (Rminus x y) (refl_eqT R (Rminus x y))).
 Save.
 
+(*********)
+Lemma R_dist_plus: (a,b,c,d:R)(Rle (R_dist (Rplus a c) (Rplus b d))
+                   (Rplus (R_dist a b) (R_dist c d))).
+Intros;Unfold R_dist;
+ Replace (Rminus (Rplus a c) (Rplus b d))
+  with (Rplus (Rminus a b) (Rminus c d)).
+Exact (Rabsolu_triang (Rminus a b) (Rminus c d)).
+Ring.
+Save.
+
 (*******************************)
 (*    R is a metric space      *)
 (*******************************)
@@ -378,36 +435,27 @@ Save.
 Lemma limit_plus:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R)
    (limit1_in f D l x0)->(limit1_in g D l' x0)->
    (limit1_in [x:R](Rplus (f x) (g x)) D (Rplus l l') x0).
-Unfold limit1_in;Unfold limit_in;Simpl;Intros;
+Intros;Unfold limit1_in; Unfold limit_in; Simpl; Intros;
  Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
- Elim (H0 (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
- Clear H H0;Intros;Elim H;Elim H0;Clear H H0;Intros;
- Split with (Rmin x1 x);Split.
-Elim (Rmin_Rgt x1 x R0);Intros a b;
- Apply (b (conj (Rgt x1 R0) (Rgt x R0) H H2));Clear a b.
-Intros;Elim H4;Clear H4;Intros;Elim (Rmin_Rgt x1 x (R_dist x2 x0));
- Intros a b;Clear b;Unfold Rgt in a;Elim (a H5);Clear H5 a;Intros;
- Generalize (H0 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H4 H5)); 
- Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6));
- Clear H0 H3 H5 H6;Intros;
- Generalize (Rplus_lt (R_dist (f x2) l) 
-                     (Rmult eps (Rinv (Rplus R1 R1))) 
-                     (R_dist (g x2) l')
-                     (Rmult eps (Rinv (Rplus R1 R1))) H3 H0);
- Clear H0 H3 H4;Intro;Rewrite (eps2 eps) in H0;Unfold R_dist;
- Unfold Rminus;Rewrite (Rplus_sym l l');Rewrite (Ropp_distr1 l' l);
- Rewrite <-(Rplus_assoc (Rplus (f x2) (g x2)) (Ropp l') (Ropp l));
- Rewrite (Rplus_assoc (f x2) (g x2) (Ropp l'));
- Rewrite (Rplus_sym (Rplus (f x2) (Rplus (g x2) (Ropp l'))) 
-   (Ropp l));
- Rewrite <-(Rplus_assoc (Ropp l) (f x2) (Rplus (g x2) (Ropp l')));
- Rewrite (Rplus_sym (Ropp l) (f x2));
- Fold (Rminus (f x2) l);Fold (Rminus (g x2) l');Unfold R_dist in H0;
- Apply (Rle_lt_trans 
-  (Rabsolu (Rplus (Rminus (f x2) l) (Rminus (g x2) l')))
-  (Rplus (Rabsolu (Rminus (f x2) l)) (Rabsolu (Rminus (g x2) l')))
-  eps 
-  (Rabsolu_triang (Rminus (f x2) l) (Rminus (g x2) l')) H0).
+  Elim (H0 (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
+ Simpl;Clear H H0; Intros; Elim H; Elim H0; Clear H H0; Intros;
+  Split with (Rmin x1 x); Split.
+Exact (Rmin_Rgt_r x1 x R0 (conj ? ? H H2)).
+Intros;Elim H4; Clear H4; Intros;
+ Cut (Rlt (Rplus (R_dist (f x2) l) (R_dist (g x2) l')) eps).
+ Cut (Rle (R_dist (Rplus (f x2) (g x2)) (Rplus l l'))
+      (Rplus (R_dist (f x2) l) (R_dist (g x2) l'))).
+Exact (Rle_lt_trans ? ? ?).
+Exact (R_dist_plus ? ? ? ?).
+Elim (Rmin_Rgt_l x1 x (R_dist x2 x0) H5); Clear H5; Intros.
+Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6));
+ Generalize (H0 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H4 H5));
+ Intros;
+ Replace eps
+ with (Rplus (Rmult eps (Rinv (Rplus R1 R1)))
+        (Rmult eps (Rinv (Rplus R1 R1)))).
+Exact (Rplus_lt ? ? ? ? H7 H8).
+Exact (eps2 eps).
 Save.
 
 (*********)
@@ -441,494 +489,71 @@ Save.
 Lemma limit_mul:(f,g:R->R)(D:R->Prop)(l,l':R)(x0:R)
    (limit1_in f D l x0)->(limit1_in g D l' x0)->
    (limit1_in [x:R](Rmult (f x) (g x)) D (Rmult l l') x0).
-Unfold limit1_in;Unfold limit_in;Simpl;Intros;
- Elim (Req_EM l R0);Elim (Req_EM l' R0);Intros.
-(**)
-Rewrite H2;Rewrite H3;Rewrite H2 in H0;Rewrite H3 in H;
- Rewrite (Rmult_Or R0);Unfold R_dist;Unfold R_dist in H H0;
- Elim (H eps H1);Clear H;Unfold 1 Rgt in H0;Elim (H0 R1 Rlt_R0_R1);
- Clear H0;Intros;Elim H;Elim H0;Clear H H0;Intros;
- Split with (Rmin x1 x);Split.
-Elim (Rmin_Rgt x1 x R0);Intros a b;
- Apply (b (conj (Rgt x1 R0) (Rgt x R0) H H4));Clear a b.
-Intros;Elim H6;Clear H6;Intros;Elim (Rmin_Rgt x1 x (R_dist x2 x0));
- Intros a b;Clear b;Unfold Rgt in a;Elim (a H7);Clear H7 a;Intros;
- Unfold R_dist in H7 H8;
- Generalize (H0 x2 (conj (D x2) 
-          (Rlt (Rabsolu (Rminus x2 x0)) x1) H6 H7));
- Generalize (H5 x2 (conj (D x2) 
-          (Rlt (Rabsolu (Rminus x2 x0)) x) H6 H8));Intros;
- Clear H0 H5 H7 H8;Rewrite (minus_R0 (g x2)) in H9;
- Rewrite (minus_R0 (f x2)) in H10;
- Rewrite (minus_R0 (Rmult (f x2) (g x2)));
- Generalize Rlt_R0_R1;Intro;Fold (Rgt R1 R0) in H0;
- Rewrite (Rabsolu_mult (f x2) (g x2));
- Rewrite <-(let (H1,H2)=(Rmult_ne eps) in H1);
- Generalize (Rabsolu_pos (g x2));Unfold Rle;Intro;Elim H5;Clear H5;
- Intro.
-Apply (Rmult_lt (Rabsolu (f x2)) eps (Rabsolu (g x2)) R1 H5 H1 H10 H9).
-Rewrite <-H5;Rewrite (Rmult_Or (Rabsolu (f x2))); 
- Rewrite (let (H1,H2)=(Rmult_ne eps) in H1);Unfold Rgt in H1;Assumption.
-(**)
-Rewrite H3;Rewrite H3 in H;Rewrite (Rmult_Ol l');
- Elim (H0 (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));Intros;
- Elim H4;Clear H4;Intros;
- Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;Elim (H R1 H6);Intros;
- Elim H7;Clear H7;Intros;
- Cut (Rgt (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l')))) R0).
-Intro;Elim (H (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l')))) H9);
- Intros;Elim H10;Clear H10;Intros;Split with (Rmin (Rmin x x1) x2);
- Split.
-Elim (Rmin_Rgt (Rmin x x1) x2 R0);Intros;Elim (Rmin_Rgt x x1 R0);Intros;
- Generalize (H15 (conj (Rgt x R0) (Rgt x1 R0) H4 H7));Clear H14 H15;
- Intro;Clear H12;
- Apply (H13 (conj (Rgt (Rmin x x1) R0) (Rgt x2 R0) H14 H10)).
-Intros;Elim H12;Clear H12;Intros;
- Elim (Rmin_Rgt (Rmin x x1) x2 (R_dist x3 x0));Intros;Clear H15;
- Unfold 1 Rgt in H14;Elim (H14 H13);Clear H14;Intros;Unfold Rgt in H15;
- Clear H13;Elim (Rmin_Rgt x x1 (R_dist x3 x0));Intros;
- Elim (H13 H14);Clear H14 H13 H16;Intros;Unfold Rgt in H13 H14;
- Generalize (H5 x3 (conj (D x3) (Rlt (R_dist x3 x0) x) H12 H13));
- Generalize (H8 x3 (conj (D x3) (Rlt (R_dist x3 x0) x1) H12 H14));
- Generalize (H11 x3 (conj (D x3) (Rlt (R_dist x3 x0) x2) H12 H15));
- Clear H5 H8 H11 H15 H13 H14 H12;Intros;Unfold R_dist in H5 H8 H11;
- Unfold R_dist;Rewrite (minus_R0 (Rmult (f x3) (g x3)));
- Rewrite (minus_R0 (f x3)) in H5;Rewrite (minus_R0 (f x3)) in H8;
- Rewrite <-(let (H1,H2)=(Rplus_ne (Rmult (f x3) (g x3))) in H1);
- Rewrite <-(Rplus_Ropp_l (Rmult (f x3) l'));Rewrite (Rmult_sym (f x3) l');
- Rewrite <-(Ropp_mul1 l' (f x3));
- Rewrite (Rmult_sym (Ropp l') (f x3));
- Rewrite <-(Rplus_assoc (Rmult (f x3) (g x3)) 
-                     (Rmult (f x3) (Ropp l')) (Rmult l' (f x3)));
- Rewrite <-(Rmult_Rplus_distr (f x3) (g x3) (Ropp l'));Fold (Rminus (g x3) l');
- Generalize (Rabsolu_triang (Rmult (f x3) (Rminus (g x3) l'))
-                            (Rmult l' (f x3)));Intro;
- Apply (Rle_lt_trans 
-   (Rabsolu (Rplus (Rmult (f x3) (Rminus (g x3) l')) (Rmult l' (f x3))))
-   (Rplus (Rabsolu (Rmult (f x3) (Rminus (g x3) l')))
-         (Rabsolu (Rmult l' (f x3)))) eps H12);Clear H12;
- Rewrite (Rabsolu_mult (f x3) (Rminus (g x3) l'));
- Rewrite (Rabsolu_mult l' (f x3));
- Elim (Req_EM (f x3) R0);Intros.
-Rewrite H12;Rewrite Rabsolu_R0;
- Rewrite (Rmult_Ol (Rabsolu (Rminus (g x3) l')));
- Rewrite (Rmult_Or (Rabsolu l'));
- Rewrite (let (H1,H2)=(Rplus_ne R0) in H1); 
- Unfold Rgt in H1;Assumption.
-Generalize (Rabsolu_pos_lt (f x3) H12);Intro;
- Fold (Rgt (Rabsolu (f x3)) R0) in H13;
- Generalize (Rmult_lt (Rabsolu (Rminus (g x3) l')) 
-                      (Rmult eps (Rinv (Rplus R1 R1)))
-                      (Rabsolu (f x3)) R1 H13 (eps2_Rgt_R0 eps H1) 
-         H11 H8);Intro;
- Generalize (Rlt_monotony (Rabsolu l') (Rabsolu (f x3))
-   (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))))  
-      (Rabsolu_pos_lt l' H2) H5);Clear H5 H8 H11 H12 H13;Intro;
- Rewrite (Rmult_sym (Rabsolu (Rminus (g x3) l')) (Rabsolu (f x3))) 
-  in H14;Generalize (Rplus_lt 
-     (Rmult (Rabsolu (f x3)) (Rabsolu (Rminus (g x3) l')))
-     (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
-     (Rmult (Rabsolu l') (Rabsolu (f x3)))
-     (Rmult (Rabsolu l')
-        (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))))) H14 H5);
- Clear H5 H14;Intro;
- Cut eps==(Rplus (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
-             (Rmult (Rabsolu l')
-               (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l')))))).
-Intro;Rewrite <-H8 in H5;Assumption.
-Rewrite (let (H1,H2)=
-  (Rmult_ne (Rmult eps (Rinv (Rplus R1 R1)))) in H1);
- Cut ~(Rabsolu l')==R0. 
-Intro;Rewrite (Rinv_Rmult (Rplus R1 R1) (Rabsolu l'));Auto.
-Rewrite (Rmult_sym (Rabsolu l') 
-  (Rmult eps (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l')))));
- Rewrite (Rmult_assoc eps 
-    (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l')))
-    (Rabsolu l'));
- Rewrite (Rmult_assoc (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l'))
-   (Rabsolu l'));
- Rewrite (Rinv_l (Rabsolu l') H8);
- Rewrite (let (H1,H2)=
-  (Rmult_ne (Rinv (Rplus R1 R1))) in H1);
- Apply sym_eqT;Apply eps2.
-Apply (imp_not_Req (Rplus R1 R1) R0);Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H11);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H12;
- Apply (Rlt_trans R0 R1 (Rplus R1 R1) H11 H12).
-Generalize (Rabsolu_pos_lt l' H2);Intro;
- Apply (imp_not_Req (Rabsolu l') R0);Auto.
-Unfold Rgt;Unfold Rgt in H1;
- Rewrite <-(Rmult_Or (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))));
- Rewrite (Rmult_sym eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))));
- Apply (Rlt_monotony (Rinv (Rmult (Rplus R1 R1) (Rabsolu l'))) R0 eps);
- Auto.
-Apply (Rlt_Rinv (Rmult (Rplus R1 R1) (Rabsolu l')));
- Generalize (Rabsolu_pos_lt l' H2);
- Clear H H0 H3 H4 H5 H7 H8 f g D l x0 x x1;Intro;
- Rewrite <-(Rmult_Or (Rplus R1 R1)); 
- Apply (Rlt_monotony (Rplus R1 R1) R0 (Rabsolu l'));Auto.
-Unfold Rgt in H6;Generalize (Rlt_compatibility R1 R0 R1 H6);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H0;
- Apply (Rlt_trans R0 R1 (Rplus R1 R1) H6 H0).
-(**)
-Rewrite H2;Rewrite H2 in H0;Rewrite (Rmult_Or l);
- Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));Intros;
- Elim H4;Clear H4;Intros;
- Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;Elim (H0 R1 H6);Intros;
- Elim H7;Clear H7;Intros;
- Cut (Rgt (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l)))) R0).
-Intro;Elim (H0 (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l)))) H9);
- Intros;Elim H10;Clear H10;Intros;Split with (Rmin (Rmin x x1) x2);
- Split.
-Elim (Rmin_Rgt (Rmin x x1) x2 R0);Intros;Elim (Rmin_Rgt x x1 R0);Intros;
- Generalize (H15 (conj (Rgt x R0) (Rgt x1 R0) H4 H7));Clear H14 H15;
- Intro;Clear H12;
- Apply (H13 (conj (Rgt (Rmin x x1) R0) (Rgt x2 R0) H14 H10)).
-Intros;Elim H12;Clear H12;Intros;
- Elim (Rmin_Rgt (Rmin x x1) x2 (R_dist x3 x0));Intros;Clear H15;
- Unfold 1 Rgt in H14;Elim (H14 H13);Clear H14;Intros;Unfold Rgt in H15;
- Clear H13;Elim (Rmin_Rgt x x1 (R_dist x3 x0));Intros;
- Elim (H13 H14);Clear H14 H13 H16;Intros;Unfold Rgt in H13 H14;
- Generalize (H5 x3 (conj (D x3) (Rlt (R_dist x3 x0) x) H12 H13));
- Generalize (H8 x3 (conj (D x3) (Rlt (R_dist x3 x0) x1) H12 H14));
- Generalize (H11 x3 (conj (D x3) (Rlt (R_dist x3 x0) x2) H12 H15));
- Clear H5 H8 H11 H15 H13 H14 H12;Intros;Unfold R_dist in H5 H8 H11;
- Unfold R_dist;Rewrite (minus_R0 (Rmult (f x3) (g x3)));
- Rewrite (minus_R0 (g x3)) in H8;Rewrite (minus_R0 (g x3)) in H5;
- Rewrite <-(let (H1,H2)=(Rplus_ne (Rmult (f x3) (g x3))) in H1);
- Rewrite <-(Rplus_Ropp_l (Rmult (g x3) l));Rewrite (Rmult_sym (g x3) l);
- Rewrite <-(Ropp_mul1 l (g x3));
- Rewrite (Rmult_sym (Ropp l) (g x3));
- Rewrite <-(Rplus_assoc (Rmult (f x3) (g x3)) 
-                     (Rmult (g x3) (Ropp l)) (Rmult l (g x3)));
- Rewrite (Rmult_sym (f x3) (g x3));
- Rewrite <-(Rmult_Rplus_distr (g x3) (f x3) (Ropp l));Fold (Rminus (f x3) l);
- Generalize (Rabsolu_triang (Rmult (g x3) (Rminus (f x3) l))
-                            (Rmult l (g x3)));Intro;
- Apply (Rle_lt_trans 
-   (Rabsolu (Rplus (Rmult (g x3) (Rminus (f x3) l)) (Rmult l (g x3))))
-   (Rplus (Rabsolu (Rmult (g x3) (Rminus (f x3) l)))
-         (Rabsolu (Rmult l (g x3)))) eps H12);Clear H12;
- Rewrite (Rabsolu_mult (g x3) (Rminus (f x3) l));
- Rewrite (Rabsolu_mult l (g x3));
- Elim (Req_EM (g x3) R0);Intros.
-Rewrite H12;Rewrite Rabsolu_R0;
- Rewrite (Rmult_Ol (Rabsolu (Rminus (f x3) l)));
- Rewrite (Rmult_Or (Rabsolu l));
- Rewrite (let (H1,H2)=(Rplus_ne R0) in H1); 
- Unfold Rgt in H1;Assumption.
-Generalize (Rabsolu_pos_lt (g x3) H12);Intro;
- Fold (Rgt (Rabsolu (g x3)) R0) in H13;
- Generalize (Rmult_lt (Rabsolu (Rminus (f x3) l)) 
-                      (Rmult eps (Rinv (Rplus R1 R1)))
-                      (Rabsolu (g x3)) R1 H13 (eps2_Rgt_R0 eps H1) 
-         H11 H8);Intro;
- Generalize (Rlt_monotony (Rabsolu l) (Rabsolu (g x3))
-   (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))))  
-      (Rabsolu_pos_lt l H3) H5);Clear H5 H8 H11 H12 H13;Intro;
- Rewrite (Rmult_sym (Rabsolu (Rminus (f x3) l)) (Rabsolu (g x3))) 
-  in H14;Generalize (Rplus_lt 
-     (Rmult (Rabsolu (g x3)) (Rabsolu (Rminus (f x3) l)))
-     (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
-     (Rmult (Rabsolu l) (Rabsolu (g x3)))
-     (Rmult (Rabsolu l)
-        (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))))) H14 H5);
- Clear H5 H14;Intro;
- Cut eps==(Rplus (Rmult (Rmult eps (Rinv (Rplus R1 R1))) R1)
-             (Rmult (Rabsolu l)
-               (Rmult eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l)))))).
-Intro;Rewrite <-H8 in H5;Assumption.
-Rewrite (let (H1,H2)=
-  (Rmult_ne (Rmult eps (Rinv (Rplus R1 R1)))) in H1);
- Cut ~(Rabsolu l)==R0. 
-Intro;Rewrite (Rinv_Rmult (Rplus R1 R1) (Rabsolu l));Auto.
-Rewrite (Rmult_sym (Rabsolu l) 
-  (Rmult eps (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l)))));
- Rewrite (Rmult_assoc eps 
-    (Rmult (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l)))
-    (Rabsolu l));
- Rewrite (Rmult_assoc (Rinv (Rplus R1 R1)) (Rinv (Rabsolu l))
-   (Rabsolu l));
- Rewrite (Rinv_l (Rabsolu l) H8);
- Rewrite (let (H1,H2)=
-  (Rmult_ne (Rinv (Rplus R1 R1))) in H1);
- Apply sym_eqT;Apply eps2.
-Apply (imp_not_Req (Rplus R1 R1) R0);Right;Unfold Rgt;Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H11);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H12;
- Apply (Rlt_trans R0 R1 (Rplus R1 R1) H11 H12).
-Generalize (Rabsolu_pos_lt l H3);Intro;
- Apply (imp_not_Req (Rabsolu l) R0);Auto.
-Unfold Rgt;Unfold Rgt in H1;
- Rewrite <-(Rmult_Or (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))));
- Rewrite (Rmult_sym eps (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))));
- Apply (Rlt_monotony (Rinv (Rmult (Rplus R1 R1) (Rabsolu l))) R0 eps);
- Auto.
-Apply (Rlt_Rinv (Rmult (Rplus R1 R1) (Rabsolu l)));
- Generalize (Rabsolu_pos_lt l H3);
- Clear H H0 H2 H4 H5 H7 H8 f g D l' x0 x x1;Intro;
- Rewrite <-(Rmult_Or (Rplus R1 R1)); 
- Apply (Rlt_monotony (Rplus R1 R1) R0 (Rabsolu l));Auto.
-Unfold Rgt in H6;Generalize (Rlt_compatibility R1 R0 R1 H6);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H0;
- Apply (Rlt_trans R0 R1 (Rplus R1 R1) H6 H0).
-(**)
-Cut ~(Rplus (Rplus R1 R1) (Rplus R1 R1))==R0.
-Cut ~(Rabsolu l)==R0.
-Cut ~(Rabsolu l')==R0.
-Intros tl' tl add4;
- Elim (H (Rmult eps (Rinv (Rplus R1 R1))) (eps2_Rgt_R0 eps H1));
- Intros;Elim H4;Clear H4;Intros;
- Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;Elim (H0 R1 H6);Intros;
- Elim H7;Clear H7;Intros;
- Cut (Rgt (Rmult eps 
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))) R0).
-Cut (Rgt (Rmult eps 
- (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')))) R0).
-Intros;Elim (H0 (Rmult eps 
-   (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))) H10);
- Intros;Elim H11;Clear H11;Intros;
- Elim (H (Rmult eps 
-   (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')))) H9);
- Intros;Elim H13;Clear H13;Intros;
- Split with (Rmin (Rmin x x1) (Rmin x2 x3));Split.
-Elim (Rmin_Rgt (Rmin x x1) (Rmin x2 x3) R0);Intros;
- Elim (Rmin_Rgt x x1 R0);Elim (Rmin_Rgt x2 x3 R0);Intros;
- Apply (H16 (conj (Rgt (Rmin x x1) R0) (Rgt (Rmin x2 x3) R0) 
-  (H20 (conj (Rgt x R0) (Rgt x1 R0) H4 H7)) 
-  (H18 (conj (Rgt x2 R0) (Rgt x3 R0) H11 H13)))).
-Intros;Elim H15;Clear H15;Intros;
- Elim (Rmin_Rgt (Rmin x x1) (Rmin x2 x3) (R_dist x4 x0));Intros;
- Clear H18;Unfold 1 Rgt in H17;Elim (H17 H16);Clear H17 H16;Intros;
- Elim (Rmin_Rgt x x1 (R_dist x4 x0));
- Elim (Rmin_Rgt x2 x3 (R_dist x4 x0));Intros;
- Unfold 1 Rgt in H17;Unfold 1 Rgt in H20;Elim (H18 H17);Elim (H20 H16);
- Clear H16 H17 H18 H19 H20 H21;Intros;Unfold Rgt in H16 H17 H18 H19;
- Generalize (H5 x4 (conj (D x4) (Rlt (R_dist x4 x0) x) H15 H16));
- Generalize (H8 x4 (conj (D x4) (Rlt (R_dist x4 x0) x1) H15 H17));
- Generalize (H12 x4 (conj (D x4) (Rlt (R_dist x4 x0) x2) H15 H18));
- Generalize (H14 x4 (conj (D x4) (Rlt (R_dist x4 x0) x3) H15 H19));
- Clear H H0 H5 H8 H12 H14 H16 H17 H18 H19;Intros;
- Unfold R_dist in H H0 H5 H8;Unfold R_dist; 
- Rewrite <-(let (H1,H2)=(Rplus_ne (Rmult (f x4) (g x4))) in H1);
- Rewrite <-(Rplus_Ropp_l (Rmult (g x4) l));Rewrite (Rmult_sym (g x4) l);
- Rewrite <-(Ropp_mul1 l (g x4));
- Rewrite (Rmult_sym (Ropp l) (g x4));
- Rewrite <-(Rplus_assoc (Rmult (f x4) (g x4)) 
-                     (Rmult (g x4) (Ropp l)) (Rmult l (g x4)));
- Rewrite (Rmult_sym (f x4) (g x4));
- Rewrite <-(Rmult_Rplus_distr (g x4) (f x4) (Ropp l));Fold (Rminus (f x4) l);
- Unfold 1 Rminus;Rewrite (Rmult_sym l l');Rewrite <-(Ropp_mul1 l' l);
- Rewrite (Rmult_sym (Ropp l') l);
- Rewrite (Rplus_assoc (Rmult (g x4) (Rminus (f x4) l)) 
-                     (Rmult l (g x4)) (Rmult l (Ropp l')));
- Rewrite <-(Rmult_Rplus_distr l (g x4) (Ropp l'));
- Fold (Rminus (g x4) l');
- Generalize (Rabsolu_triang (Rmult (g x4) (Rminus (f x4) l))
-                            (Rmult l (Rminus (g x4) l')));Intro;
- Apply (Rle_lt_trans 
-   (Rabsolu (Rplus (Rmult (g x4) (Rminus (f x4) l)) 
-                  (Rmult l (Rminus (g x4) l'))))
-   (Rplus (Rabsolu (Rmult (g x4) (Rminus (f x4) l)))
-         (Rabsolu (Rmult l (Rminus (g x4) l')))) eps H12);Clear H12;
- Generalize (Rlt_monotony (Rabsolu l) (Rabsolu (Rminus (g x4) l')) 
-                      (Rmult eps
-           (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))))
-                      (Rabsolu_pos_lt l H3) H0);Intro;
- Generalize (Rlt_monotony (Rabsolu l') (Rabsolu (Rminus (f x4) l)) 
-                      (Rmult eps
-           (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l'))))
-                      (Rabsolu_pos_lt l' H2) H);Intro;
- Elim (Req_EM (f x4) l);Intros.
-Rewrite H16;Rewrite (eq_Rminus l l (refl_eqT R l));
- Rewrite (Rmult_Or (g x4));Rewrite Rabsolu_R0;
- Rewrite (let (H1,H2)=(Rplus_ne (Rabsolu (Rmult l (Rminus (g x4) l')))) 
-   in H2);Rewrite (Rabsolu_mult l (Rminus (g x4) l'));
- Apply (Rlt_trans (Rmult (Rabsolu l) (Rabsolu (Rminus (g x4) l')))
-     (Rmult (Rabsolu l)
-            (Rmult eps
-              (Rinv
-                (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))))
-     eps H12); 
- Rewrite (Rmult_sym eps 
-   (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))));
- Rewrite <-(Rmult_assoc (Rabsolu l) 
-  (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))) eps);
- Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l) add4 
-    tl);
- Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
-                     (Rinv (Rabsolu l))); 
- Rewrite <-(Rmult_assoc (Rabsolu l) (Rinv (Rabsolu l)) 
-                      (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))));
- Rewrite (Rinv_r (Rabsolu l) tl);
- Rewrite (let (H1,H2)=(Rmult_ne (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))))
-  in H2);Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
-           eps);Apply (Rlt_eps4_eps eps H1).
-Generalize Rlt_R0_R1;Fold (Rgt R1 R0);Intro;
- Cut (Rgt (Rabsolu (Rminus (f x4) l)) R0).
-Intro;
- Generalize (Rmult_lt (Rabsolu (Rminus (g x4) l')) R1 
-                     (Rabsolu (Rminus (f x4) l)) 
-                     (Rmult eps (Rinv (Rplus R1 R1)))
-                      H18 H17 H5 H8);Intro;
- Rewrite (let (H1,H2)=(Rmult_ne (Rmult eps (Rinv (Rplus R1 R1)))) in H2)
-  in H19;Generalize (Rplus_lt (Rmult (Rabsolu (Rminus (g x4) l'))
-            (Rabsolu (Rminus (f x4) l)))
-                             (Rmult eps (Rinv (Rplus R1 R1)))
-                      (Rmult (Rabsolu l') (Rabsolu (Rminus (f x4) l)))
-                      (Rmult (Rabsolu l')
-            (Rmult eps (Rinv
-                (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l')))))
-              H19 H14);Intro;
- Generalize (Rplus_lt (Rmult (Rabsolu l) (Rabsolu (Rminus (g x4) l')))
-                     (Rmult (Rabsolu l)
-            (Rmult eps
-              (Rinv
-                (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))))
-             (Rplus
-            (Rmult (Rabsolu (Rminus (g x4) l'))
-              (Rabsolu (Rminus (f x4) l)))
-            (Rmult (Rabsolu l') (Rabsolu (Rminus (f x4) l))))
-            (Rplus (Rmult eps (Rinv (Rplus R1 R1)))
-            (Rmult (Rabsolu l')
-              (Rmult eps
-                (Rinv
-              (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l'))))))
-              H12 H20);
- Clear H5 H8 H12 H14 H19 H20 H H0 H9 H10;Replace (Rplus
-            (Rmult (Rabsolu l)
-              (Rmult eps
-                (Rinv
-                  (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l)))))
-            (Rplus (Rmult eps (Rinv (Rplus R1 R1)))
-              (Rmult (Rabsolu l')
-                (Rmult eps
-                  (Rinv
-                    (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1))
-                      (Rabsolu l'))))))) with eps.
-Intro;Rewrite (Rplus_sym (Rabsolu (Rmult (g x4) (Rminus (f x4) l)))
-           (Rabsolu (Rmult l (Rminus (g x4) l'))));
- Pattern 2 (g x4);
- Rewrite <-(let (H1,H2)=(Rplus_ne (g x4)) in H1);
- Rewrite <-(Rplus_Ropp_r l');Rewrite <-(Rplus_assoc (g x4) l' (Ropp l')); 
- Rewrite (Rmult_sym (Rplus (Rplus (g x4) l') (Ropp l')) 
-                      (Rminus (f x4) l));
- Rewrite (Rabsolu_mult (Rminus (f x4) l)
-                      (Rplus (Rplus (g x4) l') (Ropp l')));
- Rewrite (Rmult_sym (Rabsolu (Rminus (g x4) l'))
-                      (Rabsolu (Rminus (f x4) l))) in H;
- Rewrite (Rmult_sym (Rabsolu l') 
-                      (Rabsolu (Rminus (f x4) l))) in H;
- Rewrite <-(Rmult_Rplus_distr (Rabsolu (Rminus (f x4) l))
-                  (Rabsolu (Rminus (g x4) l'))
-                  (Rabsolu l')) in H;
- Rewrite <-(Rabsolu_mult l (Rminus (g x4) l')) in H;
- Rewrite (Rplus_assoc (g x4) l' (Ropp l'));
- Rewrite (Rplus_sym l' (Ropp l'));
- Rewrite <-(Rplus_assoc (g x4) (Ropp l') l');
- Fold (Rminus (g x4) l');
- Generalize (Rabsolu_triang (Rminus (g x4) l') l');Intro;
- Unfold Rle in H0;Elim H0;Clear H0;Intro.
-Unfold Rgt in H18.
- Generalize (Rlt_monotony (Rabsolu (Rminus (f x4) l)) 
-        (Rabsolu (Rplus (Rminus (g x4) l') l'))
-        (Rplus (Rabsolu (Rminus (g x4) l')) (Rabsolu l')) 
-        H18 H0);Intro;
- Generalize (Rlt_compatibility (Rabsolu (Rmult l (Rminus (g x4) l')))
-        (Rmult (Rabsolu (Rminus (f x4) l))
-           (Rabsolu (Rplus (Rminus (g x4) l') l')))
-        (Rmult (Rabsolu (Rminus (f x4) l))
-           (Rplus (Rabsolu (Rminus (g x4) l')) (Rabsolu l')))
-        H5);Clear H0 H5;Intro;
- Apply (Rlt_trans (Rplus (Rabsolu (Rmult l (Rminus (g x4) l')))
-           (Rmult (Rabsolu (Rminus (f x4) l))
-             (Rabsolu (Rplus (Rminus (g x4) l') l'))))
-                   (Rplus (Rabsolu (Rmult l (Rminus (g x4) l')))
-           (Rmult (Rabsolu (Rminus (f x4) l))
-             (Rplus (Rabsolu (Rminus (g x4) l')) (Rabsolu l'))))
-                   eps H0 H).
-Rewrite H0;Assumption. 
-Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1))
-                            (Rabsolu l) add4 tl);
- Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1))
-                            (Rabsolu l') add4 tl');
- Rewrite (Rmult_sym eps (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
-              (Rinv (Rabsolu l))));
- Rewrite (Rmult_sym eps (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))
-              (Rinv (Rabsolu l'))));
- Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
-                      (Rinv (Rabsolu l)));
- Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
-                      (Rinv (Rabsolu l')));
- Rewrite (Rmult_assoc (Rinv (Rabsolu l)) 
-        (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps);
- Rewrite (Rmult_assoc (Rinv (Rabsolu l')) 
-        (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps);
- Rewrite <-(Rmult_assoc (Rabsolu l) (Rinv (Rabsolu l))
-        (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps));
- Rewrite <-(Rmult_assoc (Rabsolu l') (Rinv (Rabsolu l'))
-        (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps));
- Rewrite (Rinv_r (Rabsolu l) tl);Rewrite (Rinv_r (Rabsolu l') tl');
- Rewrite (let (H1,H2)=(Rmult_ne 
-      (Rmult (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps)) in H2);
- Rewrite (Rmult_sym (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) eps);
- Rewrite (Rplus_sym (Rmult eps (Rinv (Rplus R1 R1)))
-                  (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1)))));
- Rewrite <- (Rplus_assoc 
-     (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))))
-     (Rmult eps (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))))
-     (Rmult eps (Rinv (Rplus R1 R1))));
- Rewrite eps4;Rewrite eps2;Trivial.
-Unfold Rgt;Apply (Rabsolu_pos_lt (Rminus (f x4) l));Red;Intro;Elim H16;
- Apply (Rminus_eq (f x4) l H18).
-Apply (Rmult_gt eps 
-  (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l'))) H1);
- Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l') 
-           add4 tl'); 
- Apply (Rmult_gt (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
-  (Rinv (Rabsolu l'))).
-Unfold Rgt;Apply (Rlt_Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))).
-Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H9);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H10;
- Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H9 H10);Intro;
- Clear H9 H10;
- Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H11);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H9;
- Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
-    H11 H9).
-Unfold Rgt;Apply (Rlt_Rinv (Rabsolu l') (Rabsolu_pos_lt l' H2)).
-Apply (Rmult_gt eps 
-  (Rinv (Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l))) H1);
- Rewrite (Rinv_Rmult (Rplus (Rplus R1 R1) (Rplus R1 R1)) (Rabsolu l) 
-           add4 tl); 
- Apply (Rmult_gt (Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))) 
-  (Rinv (Rabsolu l))).
-Unfold Rgt;Apply (Rlt_Rinv (Rplus (Rplus R1 R1) (Rplus R1 R1))).
-Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H9);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H10;
- Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H9 H10);Intro;
- Clear H9 H10;
- Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H11);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H9;
- Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
-    H11 H9).
-Unfold Rgt;Apply (Rlt_Rinv (Rabsolu l) (Rabsolu_pos_lt l H3)).
-Generalize (Rabsolu_pos_lt l' H2);Intro;
- Apply (imp_not_Req (Rabsolu l') R0);Auto.
-Generalize (Rabsolu_pos_lt l H3);Intro;
- Apply (imp_not_Req (Rabsolu l) R0);Auto.
-Apply (imp_not_Req (Rplus (Rplus R1 R1) (Rplus R1 R1)) R0);Right;Unfold Rgt;
- Generalize Rlt_R0_R1;Intro;
- Generalize (Rlt_compatibility R1 R0 R1 H4);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne R1) in H1) in H5;
- Generalize (Rlt_trans R0 R1 (Rplus R1 R1) H4 H5);Intro;
- Clear H4 H5;
- Generalize (Rlt_compatibility (Rplus R1 R1) R0 (Rplus R1 R1) H6);Intro;
- Rewrite (let (H1,H2)=(Rplus_ne (Rplus R1 R1)) in H1) in H4;
- Apply (Rlt_trans R0 (Rplus R1 R1) (Rplus (Rplus R1 R1) (Rplus R1 R1))
-    H6 H4).
+Intros;Unfold limit1_in; Unfold limit_in; Simpl; Intros; 
+ Elim (H (Rmin R1 (Rmult eps (mul_factor l l'))) 
+                   (mul_factor_gt_f eps l l' H1));
+ Elim (H0 (Rmult eps (mul_factor l l')) (mul_factor_gt eps l l' H1));
+ Clear H H0; Simpl; Intros; Elim H; Elim H0; Clear H H0; Intros;
+ Split with (Rmin x1 x); Split.
+Exact (Rmin_Rgt_r x1 x R0 (conj ? ? H H2)).
+Intros; Elim H4; Clear H4; Intros;Unfold R_dist;
+ Replace (Rminus (Rmult (f x2) (g x2)) (Rmult l l')) with 
+     (Rplus (Rmult (f x2) (Rminus (g x2) l')) (Rmult l' (Rminus (f x2) l))).
+Cut (Rlt (Rplus (Rabsolu (Rmult (f x2) (Rminus (g x2) l'))) (Rabsolu (Rmult l' 
+ (Rminus (f x2) l)))) eps). 
+Cut (Rle (Rabsolu (Rplus (Rmult (f x2) (Rminus (g x2) l')) (Rmult l' (Rminus 
+  (f x2) l)))) (Rplus (Rabsolu (Rmult (f x2) (Rminus (g x2) l'))) (Rabsolu 
+        (Rmult l' (Rminus (f x2) l))))).
+Exact (Rle_lt_trans ? ? ?).
+Exact (Rabsolu_triang ? ?).
+Rewrite (Rabsolu_mult (f x2) (Rminus (g x2) l'));
+ Rewrite (Rabsolu_mult l' (Rminus (f x2) l));
+ Cut (Rle (Rplus (Rmult (Rplus R1 (Rabsolu l)) (Rmult eps (mul_factor l l'))) 
+   (Rmult (Rabsolu l') (Rmult eps (mul_factor l l')))) eps).
+Cut (Rlt (Rplus (Rmult (Rabsolu (f x2)) (Rabsolu (Rminus (g x2) l'))) (Rmult 
+  (Rabsolu l') (Rabsolu (Rminus (f x2) l)))) (Rplus (Rmult (Rplus R1 (Rabsolu 
+     l)) (Rmult eps (mul_factor l l'))) (Rmult (Rabsolu l') (Rmult eps 
+      (mul_factor l l'))))).
+Exact (Rlt_le_trans ? ? ?).
+Elim (Rmin_Rgt_l x1 x (R_dist x2 x0) H5); Clear H5; Intros;
+ Generalize (H0 x2 (conj (D x2) (Rlt (R_dist x2 x0) x1) H4 H5));Intro;
+ Generalize (Rmin_Rgt_l ? ? ? H7);Intro;Elim H8;Intros;Clear H0 H8;
+ Apply Rplus_lt_le_lt.
+Apply Rmult_lt_0.
+Apply Rle_sym1.
+Exact (Rabsolu_pos (Rminus (g x2) l')).
+Rewrite (Rplus_sym R1 (Rabsolu l));Unfold Rgt;Apply Rlt_r_plus_R1;
+ Exact (Rabsolu_pos l).
+Unfold R_dist in H9;
+ Apply (Rlt_anti_compatibility (Ropp (Rabsolu l)) (Rabsolu (f x2)) 
+     (Rplus R1 (Rabsolu l))).
+Rewrite <- (Rplus_assoc (Ropp (Rabsolu l)) R1 (Rabsolu l));
+ Rewrite (Rplus_sym (Ropp (Rabsolu l)) R1);
+ Rewrite (Rplus_assoc R1 (Ropp (Rabsolu l)) (Rabsolu l));
+ Rewrite (Rplus_Ropp_l (Rabsolu l));
+ Rewrite (proj1 ? ? (Rplus_ne R1));
+ Rewrite (Rplus_sym (Ropp (Rabsolu l)) (Rabsolu (f x2)));
+ Generalize H9;
+Cut (Rle (Rminus (Rabsolu (f x2)) (Rabsolu l)) (Rabsolu (Rminus (f x2) l))).
+Exact (Rle_lt_trans ? ? ?).
+Exact (Rabsolu_triang_inv ? ?).
+Generalize (H3 x2 (conj (D x2) (Rlt (R_dist x2 x0) x) H4 H6));Trivial.
+Apply Rle_monotony.
+Exact (Rabsolu_pos l').
+Unfold Rle;Left;Assumption.
+Rewrite (Rmult_sym (Rplus R1 (Rabsolu l)) (Rmult eps (mul_factor l l')));
+ Rewrite (Rmult_sym (Rabsolu l') (Rmult eps (mul_factor l l')));
+ Rewrite <- (Rmult_Rplus_distr
+           (Rmult eps (mul_factor l l'))
+           (Rplus R1 (Rabsolu l))
+           (Rabsolu l'));
+ Rewrite (Rmult_assoc eps (mul_factor l l') (Rplus (Rplus R1 (Rabsolu l)) 
+      (Rabsolu l')));
+ Rewrite (Rplus_assoc R1 (Rabsolu l) (Rabsolu l'));Unfold mul_factor;
+ Rewrite (Rinv_l (Rplus R1 (Rplus (Rabsolu l) (Rabsolu l'))) 
+  (mul_factor_wd l l'));
+ Rewrite (proj1 ? ? (Rmult_ne eps));Apply eq_Rle;Trivial.
+Ring.
 Save.
 
 (*********)
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
new file mode 100644
index 000000000..8e07739c3
--- /dev/null
+++ b/theories/Reals/Rsyntax.v
@@ -0,0 +1,182 @@
+(* $Id$ *)
+
+Require Export Rdefinitions.
+
+Axiom NRplus : R->R->R.
+
+Grammar rnatural ident :=
+  nat_id [ prim:var($id) ] -> [$id]
+
+with rnegnumber := 
+  neg_expr [ "-" rnumber ($c) ] -> [<<(Ropp $c)>>] 
+
+with rnumber :=
+
+with rformula :=
+  form_expr [ rexpr($p) ] -> [$p]
+| form_eq [ rexpr($p) "==" rexpr($c) ] -> [<<(eqT R $p $c)>>]
+| form_le [ rexpr($p) "<=" rexpr($c) ] -> [<<(Rle $p $c)>>]
+| form_lt [ rexpr($p) "<" rexpr($c) ] -> [<<(Rlt $p $c)>>]
+| form_ge [ rexpr($p) ">=" rexpr($c) ] -> [<<(Rge $p $c)>>]
+| form_gt [ rexpr($p) ">" rexpr($c) ] -> [<<(Rgt $p $c)>>]
+| form_eq_eq [ rexpr($p) "==" rexpr($c) "==" rexpr($c1) ]
+              -> [<<(eqT R $p $c)/\(eqT R $c $c1)>>]
+| form_le_le [ rexpr($p) "<=" rexpr($c) "<=" rexpr($c1) ]
+              -> [<<(Rle $p $c)/\(Rle $c $c1)>>]
+| form_le_lt [ rexpr($p) "<=" rexpr($c) "<" rexpr($c1) ]
+              -> [<<(Rle $p $c)/\(Rlt $c $c1)>>]
+| form_lt_le [ rexpr($p) "<" rexpr($c) "<=" rexpr($c1) ]
+              -> [<<(Rlt $p $c)/\(Rle $c $c1)>>]
+| form_lt_lt [ rexpr($p) "<" rexpr($c) "<" rexpr($c1) ]
+              -> [<<(Rlt $p $c)/\(Rlt $c $c1)>>]
+| form_neq  [ rexpr($p) "<>" rexpr($c) ] -> [<< ~(eqT R $p $c)>>]
+
+with rexpr :=
+  expr_plus [ rexpr($p) "+" rexpr($c) ] -> [<<(Rplus $p $c)>>]
+| expr_minus [ rexpr($p) "-" rexpr($c) ] -> [<<(Rminus $p $c)>>]
+| rexpr2 [ rexpr2($e) ] -> [$e]
+
+with rexpr2 :=
+  expr_mult [ rexpr2($p) "*" rexpr2($c) ] -> [<<(Rmult $p $c)>>]
+| rexpr0 [ rexpr0($e) ] -> [$e]
+
+
+with rexpr0 :=
+  expr_id [ constr:global($c) ] -> [$c]
+| expr_com [ "[" constr:constr($c) "]" ] -> [$c]
+| expr_appl [ "(" rapplication($a) ")" ] -> [$a]
+| expr_num [ rnumber($s) ] -> [$s ]
+| expr_negnum [ "-" rnegnumber($n) ] -> [ $n ]
+| expr_div [ rexpr0($p) "/" rexpr0($c) ] -> [<<(Rdiv $p $c)>>]
+| expr_opp [ "-" rexpr0($c) ] -> [<<(Ropp $c)>>] 
+| expr_inv [ "1" "/" rexpr0($c) ] -> [<<(Rinv $c)>>]
+
+with rapplication :=
+  apply [ rapplication($p) rexpr($c1) ] -> [<<($p $c1)>>]
+| pair [ rexpr($p) "," rexpr($c) ] -> [<<($p, $c)>>]
+| appl0 [ rexpr($a) ] -> [$a].
+
+
+Grammar command command0 :=
+  r_in_com [ "``" rnatural:rformula($c) "``" ] -> [$c].
+
+Grammar command atomic_pattern :=
+  r_in_pattern [ "``" rnatural:rnumber($c) "``" ] -> [$c].   
+
+(** pp **)
+(* pb: on rajoute des () lorsque les constantes terminent par 1 lors de
+l'appel avec NRplus *)
+
+
+
+Syntax constr
+  level 0:
+   Rle [ (Rle $n1 $n2) ] -> 
+      [[<hov 0> "``" (REXPR $n1) [1 0] "<= " (REXPR $n2) "``"]]
+  | Rlt [ (Rlt $n1 $n2) ] -> 
+      [[<hov 0> "``" (REXPR $n1) [1 0] "< "(REXPR $n2) "``" ]]
+  | Rge [ (Rge $n1 $n2) ] -> 
+      [[<hov 0> "``" (REXPR $n1) [1 0] ">= "(REXPR $n2) "``" ]]
+  | Rgt [ (Rgt $n1 $n2) ] -> 
+      [[<hov 0> "``" (REXPR $n1) [1 0] "> "(REXPR $n2) "``" ]]
+  | Req [ (eqT R $n1 $n2) ] -> 
+      [[<hov 0> "``" (REXPR $n1) [1 0] "== "(REXPR $n2)"``"]]
+  | Rneq [ ~(eqT R $n1 $n2) ] ->
+      [[<hov 0> "``" (REXPR $n1) [1 0] "<> "(REXPR $n2) "``"]]
+  | Rle_Rle [ (Rle $n1 $n2)/\(Rle $n2 $n3) ] ->
+      [[<hov 0> "``" (REXPR $n1) [1 0] "<= " (REXPR $n2)
+                                [1 0] "<= " (REXPR $n3) "``"]]
+  | Rle_Rlt [ (Rle $n1 $n2)/\(Rlt $n2 $n3) ] ->
+      [[<hov 0> "``" (REXPR $n1) [1 0] "<= "(REXPR $n2)
+                                [1 0] "< " (REXPR $n3) "``"]]
+  | Rlt_Rle [ (Rlt $n1 $n2)/\(Rle $n2 $n3) ] ->
+      [[<hov 0> "``" (REXPR $n1) [1 0] "< " (REXPR $n2)
+                                [1 0] "<= " (REXPR $n3) "``"]]
+  | Rlt_Rlt [ (Rlt $n1 $n2)/\(Rlt $n2 $n3) ] ->
+      [[<hov 0> "``" (REXPR $n1) [1 0] "< " (REXPR $n2)
+                                [1 0] "< " (REXPR $n3) "``"]]
+  | Rzero [ R0 ] -> ["``0``"]
+  | Rone [ R1 ] -> ["``1``"]
+  | Rconst [(Rplus $r R1)] -> [$r:"r_printer"]
+  ;
+
+  level 7:
+    Rplus [ (Rplus $n1 $n2) ]
+      -> [ [<hov 0> "``"(REXPR $n1):E "+"  [0 0] (REXPR $n2):L "``"] ]
+   | Rminus [ (Rminus $n1 $n2) ]
+      -> [ [<hov 0> "``"(REXPR $n1):E "-" [0 0] (REXPR $n2):L "``"] ]
+  ;
+
+  level 6:
+    Rmult [ (Rmult $n1 $n2) ]
+      -> [ [<hov 0> "``"(REXPR $n1):E "*" [0 0] (REXPR $n2):L "``"] ]
+    |Rdiv [ (Rdiv $n1 $n2) ]
+      -> [ [<hov 0> "``"(REXPR $n1):E "/" [0 0] (REXPR $n2):L "``"] ]
+  ;
+
+  level 8:
+    Ropp [(Ropp $n1)] -> [ [<hov 0> "``" "-"(REXPR $n1):E "``"] ]
+    |Rinv [(Rinv $n1)] -> [ [<hov 0> "``" "1""/"(REXPR $n1):E "``"] ]
+  ;
+
+  level 0:
+    rescape_inside [<< (REXPR $r) >>] -> [ "[" $r:E "]" ]
+  ;
+
+  level 4:
+    Rappl_inside [<<(REXPR (APPLIST $h ($LIST $t)))>>]
+ -> [ [<hov 0> "("(REXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E ")"] ]
+  | Rappl_inside_tail [<<(APPLINSIDETAIL $h ($LIST $t))>>]
+      -> [(REXPR $h):E [1 0] (APPLINSIDETAIL ($LIST $t)):E] 
+  | Rappl_inside_one [<<(APPLINSIDETAIL $e)>>] ->[(REXPR $e):E]
+  | rpair_inside [<<(REXPR <<(pair $s1 $s2 $r1 $r2)>>)>>] 
+      -> [ [<hov 0> "("(REXPR $r1):E "," [1 0] (REXPR $r2):E ")"] ]
+  ;
+
+ level 3:
+    rvar_inside [<<(REXPR ($VAR $i))>>] -> [$i]
+  | rconst_inside [<<(REXPR (CONST $c))>>] -> [(CONST $c)]
+  | rmutind_inside [<<(REXPR (MUTIND $i $n))>>] 
+      -> [(MUTIND $i $n)]
+  | rmutconstruct_inside [<<(REXPR (MUTCONSTRUCT $c1 $c2 $c3))>>]
+      -> [ (MUTCONSTRUCT $c1 $c2 $c3) ]
+  | rimplicit_head_inside [<<(REXPR (XTRA "!" $c))>>] -> [ $c ]
+  | rimplicit_arg_inside  [<<(REXPR (XTRA "!" $n $c))>>] -> [ ]
+
+  ;
+
+  
+  level 7:
+   Rplus_inside
+      [<<(REXPR <<(Rplus $n1 $n2)>>)>>]
+      	 -> [ (REXPR $n1):E "+" [0 0] (REXPR $n2):L ]
+  | Rminus_inside
+      [<<(REXPR <<(Rminus $n1 $n2)>>)>>]
+      	 -> [ (REXPR $n1):E "-" [0 0] (REXPR $n2):L ]
+  | NRplus_inside
+      [<<(REXPR <<(NRplus $n1 $n2)>>)>>]
+      	 -> ["(" (REXPR $n1):E "+" [0 0] (REXPR $n2):L ")"]
+  ;
+
+  level 6:
+    Rmult_inside
+      [<<(REXPR <<(Rmult $n1 $n2)>>)>>]
+      	 -> [ (REXPR $n1):E "*" [0 0] (REXPR $n2):L ]
+    |Rdiv_inside
+      [<<(REXPR <<(Rdiv $n1 $n2)>>)>>]
+      	 -> [ (REXPR $n1):E "/" [0 0] (REXPR $n2):L ]
+  ;
+
+  level 6:
+ Ropp_inside [<<(REXPR <<(Ropp $n1)>>)>>] -> [ "-" (REXPR $n1):E  ]
+|Rinv_inside [<<(REXPR <<(Rinv $n1)>>)>>] -> [ "1""/" (REXPR $n1):E  ]
+  ;  
+
+  level 0:
+    Rzero_inside [<<(REXPR <<R0>>)>>] -> ["0"]
+  | Rone_inside [<<(REXPR <<R1>>)>>] -> ["1"]
+  | Rconst_inside [<<(REXPR <<(Rplus $r R1)>>)>>] -> [$r:"r_printer"].
+
+
+
+