update in groud_2 and models

[helm.git] / helm / software / matita / library / R / r.ma

diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index ce79a875b42437cf809d72d2433bfc9f2cb59409..f2bca131ff45cd10f8ef4b953af5dc64037eaba5 100644 (file)
--- a/helm/software/matita/library/R/r.ma
+++ b/helm/software/matita/library/R/r.ma
@@ -204,18 +204,18 @@ intros;autobatch paramodulation;
 qed. *)
 
 lemma Rtimes_x_R0 : ∀x.x * R0 = R0.
-intro; autobatch paramodulation. 
-(*
+(*intro; autobatch paramodulation.*)  
+intros;
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < (Rplus_Ropp (x*R0)) in ⊢ (? ? (? ? %) %);
 rewrite < assoc_Rplus;
 apply eq_f2;autobatch paramodulation;
-*)
+
 qed.
 
 lemma eq_Rtimes_Ropp_R1_Ropp : ∀x.x*(-R1) = -x.
-intro. autobatch paramodulation. (*
-auto paramodulation.
+intro. (*autobatch paramodulation.*) 
+
 rewrite < Rplus_x_R0 in ⊢ (? ? % ?);
 rewrite < Rplus_x_R0 in ⊢ (? ? ? %);
 rewrite < (Rplus_Ropp x) in ⊢ (? ? % ?);
@@ -225,7 +225,7 @@ rewrite < sym_Rplus in ⊢ (? ? (? ? %) ?);
 apply eq_f2 [reflexivity]
 rewrite < Rtimes_x_R1 in ⊢ (? ? (? % ?) ?);
 rewrite < distr_Rtimes_Rplus_l;autobatch paramodulation;
-*)
+
 qed.
 
 lemma Ropp_inv : ∀x.x = Ropp (Ropp x).
@@ -363,15 +363,13 @@ qed.
 
 lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
 intros;
-(* cut (∀x,y.x+(-x+y) = y);[2:
-intros.demodulate all.]
-applyS (Rlt_plus_l c (-?+a) (-b) ?) by (Hcut c a);
- [2: applyS Hletin;
-lapply (Rlt_plus_l (-b) ?? H); autobatch; applyS Hletin; *)
+autobatch by H, (Rlt_plus_l (-b) (a+b) c);
+(*
 rewrite < Rplus_x_R0;rewrite < (Rplus_Ropp b);
 rewrite < assoc_Rplus;
 rewrite < sym_Rplus;rewrite < sym_Rplus in ⊢ (??%);
-apply Rlt_plus_l;assumption;
+apply (Rlt_plus_l (-b) (a+b) c);assumption;
+*)
 qed.
 
 lemma Rlt_plus_r_to_l : ∀a,b,c.a < b + c → a - c < b.