(no commit message)

[helm.git] / matita / library / nat / minus.ma

diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma
index 71c2cc20552a3c6474e93ab502232f3ed202e971..f1178107a28d4f742a14942642b7daf650e97009 100644 (file)
--- 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.
@@ -140,8 +140,8 @@ intros 2.
 apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)).
 intros.simplify.reflexivity.
 intros.apply False_ind.
-apply not_le_Sn_O.
-goal 13.apply H.
+apply not_le_Sn_O;
+[2: apply H | skip].
 intros.
 simplify.apply H.apply le_S_S_to_le. apply H1.
 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.