X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fminus.ma;h=a0133e93db58f65df22e64ca4e94944a26fda79e;hb=2a31f145f58f7ba66b6445a9c8b31841054ef809;hp=71c2cc20552a3c6474e93ab502232f3ed202e971;hpb=f275a4daa42f8ab455020ec5a7ce7bf69b460c37;p=helm.git

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index 71c2cc205..a0133e93d 100644
--- a/helm/software/matita/library/nat/minus.ma
+++ b/helm/software/matita/library/nat/minus.ma
@@ -13,8 +13,6 @@
 (**************************************************************************)
 
 
-set "baseuri" "cic:/matita/nat/minus".
-
 include "nat/le_arith.ma".
 include "nat/compare.ma".
 
@@ -60,7 +58,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 +138,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 +237,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 +261,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 +285,56 @@ 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 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.
+  |intros 2.rewrite < minus_n_O.
+   intro.assumption
+  |intros.
+   simplify.
+   cut (n1 < m1+p)
+    [autobatch
+    |apply H.
+     apply H1
+    ]
+  ]
+qed.
+
+theorem lt_plus_to_lt_minus:
+\forall n,m,p. m \le n \to n < m + p \to n - m < p.
+intros 2.
+apply (nat_elim2 ? ? ? ? n m)
+  [simplify.intros 3.
+   apply (le_n_O_elim ? H).
+   simplify.intros.assumption
+  |simplify.intros.assumption.
+  |intros.
+   simplify.
+   apply H
+    [apply le_S_S_to_le.assumption
+    |apply le_S_S_to_le.apply H2
+    ]
+  ]
+qed. 
+
+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.
+qed.
+
 theorem distributive_times_minus: distributive nat times minus.
 unfold distributive.
 intros.