X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FR%2Fr.ma;h=f2bca131ff45cd10f8ef4b953af5dc64037eaba5;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=9e7ba97f5afbb4c03c5c358bcd4f9c02ad9f8dd3;hpb=765eb07cafb8a06a5027f4569ad06d805aba2488;p=helm.git

diff --git a/helm/software/matita/library/R/r.ma b/helm/software/matita/library/R/r.ma
index 9e7ba97f5..f2bca131f 100644
--- 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.