huge commit in automation:

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

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index 92324aae7610481c69fdc15a3fef5e5da8db0fb2..a8e987fc4a699cff453d0161f7c5ac71c7a61985 100644 (file)
--- a/helm/software/matita/library/nat/minus.ma
+++ b/helm/software/matita/library/nat/minus.ma
@@ -235,7 +235,8 @@ 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.
-   autobatch
+   change in H1 with (n<n1);
+   apply lt_minus_m; autobatch depth=2;
   |intros.
    generalize in match H2.
    apply (nat_case n1)
@@ -259,7 +260,7 @@ intro.elim n
    rewrite > eq_minus_S_pred.
    apply lt_pred
     [unfold lt.apply le_plus_to_minus_r.applyS H1
-    |apply H[autobatch|assumption]
+    |apply H[autobatch depth=2|assumption]
     ]
   ]
 qed.
@@ -291,18 +292,21 @@ qed.
 
 theorem lt_O_minus_to_lt: \forall a,b:nat.
 O \lt b-a \to a \lt b.
-intros.
+intros. applyS (lt_minus_to_plus O  a b). assumption;
+(*
 rewrite > (plus_n_O a).
 rewrite > (sym_plus a O).
 apply (lt_minus_to_plus O  a b).
 assumption.
+*)
 qed.
 
 theorem lt_minus_to_lt_plus:
 \forall n,m,p. n - m < p \to n < m + p.
 intros 2.
 apply (nat_elim2 ? ? ? ? n m)
-  [simplify.intros.autobatch.
+  [simplify.intros.
+   lapply depth=0 le_n; autobatch;
   |intros 2.rewrite < minus_n_O.
    intro.assumption
   |intros.
@@ -336,7 +340,7 @@ theorem minus_m_minus_mn: \forall n,m. n\le m \to n=m-(m-n).
 intros.
 apply sym_eq.
 apply plus_to_minus.
-autobatch.
+autobatch;
 qed.
 
 theorem distributive_times_minus: distributive nat times minus.
@@ -395,7 +399,7 @@ qed.
 
 theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
 p+(n-m) = n-(m-p).
-intros.
+intros. 
 apply sym_eq.
 apply plus_to_minus.
 rewrite < assoc_plus.