...

diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index d47a1dc58bd18c0dbf472e35bc2e40d2a78717cc..785ea12d4ebb2aac2754c46375afe47a4b985b16 100644 (file)
--- a/helm/software/matita/library/R/r.ma
+++ b/helm/software/matita/library/R/r.ma
@@ -58,10 +58,10 @@ axiom assoc_Rtimes : ∀x,y,z:R.(x*y)*z = x*(y*z).
 axiom Rtimes_x_R1 : ∀x.x * R1 = x.
 axiom distr_Rtimes_Rplus_l : ∀x,y,z:R.x*(y+z) = x*y + x*z.
 
-pump 200.
+(*pump 200.*)
 
 lemma distr_Rtimes_Rplus_r : ∀x,y,z:R.(x+y)*z = x*z + y*z.
-intros; demodulate all. (*autobatch paramodulation;*)
+intros; autobatch; 
 qed.
 
 (* commutative field *)
@@ -77,10 +77,12 @@ axiom trichotomy_Rlt : ∀x,y.x < y ∨ y < x ∨ x = y.
 
 lemma trans_Rle : ∀x,y,z:R.x ≤ y → y ≤ z → x ≤ z.
 intros;cases H
-[cases H1
+[cases H1; unfold; autobatch;
+|autobatch;]
+(*
  [left;autobatch
  |rewrite < H3;assumption]
-|rewrite > H2;assumption]
+|rewrite > H2;assumption]*)
 qed.
 
 axiom Rlt_plus_l : ∀x,y,z:R.x < y → z + x < z + y.
@@ -92,8 +94,20 @@ axiom Rle_times_l : ∀x,y,z:R.x ≤ y → R0 < z → z*x ≤ z*y.
 
 lemma Rle_plus_r : ∀x,y,z:R.x ≤ y → x + z ≤ y + z.
 intros;
-rewrite > sym_Rplus;rewrite > sym_Rplus in ⊢ (??%);
+applyS Rle_plus_l;
 autobatch;
+(*rewrite > sym_Rplus;rewrite > sym_Rplus in ⊢ (??%);*)
+(*applyS Rle_plus_l;
+applyS*) 
+cut ((x+z ≤ y+z) = (λx.(x+?≤ x+?)) ?);[5:simplify;
+  demodulate all;
+  autobatch paramodulation by sym_Rplus;
+
+applyS Rle_plus_l by sym_Rplus;
+
+cut ((x ≤ y) = (x+z ≤ y+z)); [2:
+  lapply (Rle_plus_l ?? z H); 
+  autobatch paramodulation by sym_Rplus,Hletin;
 qed.
 
 lemma Rle_times_r : ∀x,y,z:R.x ≤ y → R0 < z → x*z ≤ y*z.