From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 29 Apr 2009 13:37:58 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~4033
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=820e0ea35f999236e0a55915c1d40cf745ffd6b9;p=helm.git

...
---

diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index d47a1dc58..785ea12d4 100644
--- 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.