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 9e7ba97f5afbb4c03c5c358bcd4f9c02ad9f8dd3..f2bca131ff45cd10f8ef4b953af5dc64037eaba5 100644 (file)
--- a/helm/software/matita/library/R/r.ma
+++ b/helm/software/matita/library/R/r.ma
@@ -362,12 +362,13 @@ lapply (Rlt_times_l (Rinv x * Rinv y) ? ? H1)
 qed.
 
 lemma Rlt_plus_l_to_r : ∀a,b,c.a + b < c → a < c - b.
-intros; autobatch depth=4;
+intros;
+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.