X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fminus.ma;h=11585f2065706c33ba70901cd3944c4261ad775c;hb=80f85c7fb53791fd72c0e64450c3c87d8f30b84d;hp=063ab636ee8e3dae8096ba74817f48f838a98d6d;hpb=cd91767a396b7bbc72e6e3ee90a3b758421f935d;p=helm.git

diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma
index 063ab636e..11585f206 100644
--- a/matita/library/nat/minus.ma
+++ b/matita/library/nat/minus.ma
@@ -60,7 +60,7 @@ qed.
 theorem eq_minus_S_pred: \forall n,m. n - (S m) = pred(n -m).
 apply nat_elim2
   [intro.reflexivity
-  |intro.simplify.auto
+  |intro.simplify.autobatch
   |intros.simplify.assumption
   ]
 qed.
@@ -239,7 +239,7 @@ theorem lt_minus_l: \forall m,l,n:nat.
 apply nat_elim2
   [intros.apply False_ind.apply (not_le_Sn_O ? H)
   |intros.rewrite < minus_n_O.
-   auto
+   autobatch
   |intros.
    generalize in match H2.
    apply (nat_case n1)
@@ -263,7 +263,7 @@ intro.elim n
    rewrite > eq_minus_S_pred.
    apply lt_pred
     [unfold lt.apply le_plus_to_minus_r.applyS H1
-    |apply H[auto|assumption]
+    |apply H[autobatch|assumption]
     ]
   ]
 qed.
@@ -287,6 +287,15 @@ rewrite < plus_n_Sm.
 apply H.apply H1.
 qed.
 
+theorem lt_O_minus_to_lt: \forall a,b:nat.
+O \lt b-a \to a \lt b.
+intros.
+rewrite > (plus_n_O a).
+rewrite > (sym_plus a O).
+apply (lt_minus_to_plus O  a b).
+assumption.
+qed.
+
 theorem distributive_times_minus: distributive nat times minus.
 unfold distributive.
 intros.