X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fminus.ma;h=11585f2065706c33ba70901cd3944c4261ad775c;hb=6ff5322f46c2e88e07b4c345bc45edda7042128a;hp=710418d72644022cb4d799fb95f67354da4af89b;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/minus.ma b/matita/library/nat/minus.ma
index 710418d72..11585f206 100644
--- a/matita/library/nat/minus.ma
+++ b/matita/library/nat/minus.ma
@@ -57,6 +57,14 @@ intros.rewrite < H.reflexivity.
 apply le_S_S_to_le. assumption.
 qed.
 
+theorem eq_minus_S_pred: \forall n,m. n - (S m) = pred(n -m).
+apply nat_elim2
+  [intro.reflexivity
+  |intro.simplify.autobatch
+  |intros.simplify.assumption
+  ]
+qed.
+
 theorem plus_minus:
 \forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
 intros 2.
@@ -132,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.
@@ -226,6 +234,49 @@ rewrite > plus_n_Sm.assumption.
 qed.
 
 (* minus and lt - to be completed *)
+theorem lt_minus_l: \forall m,l,n:nat. 
+  l < m \to m \le n \to n - m < n - l.
+apply nat_elim2
+  [intros.apply False_ind.apply (not_le_Sn_O ? H)
+  |intros.rewrite < minus_n_O.
+   autobatch
+  |intros.
+   generalize in match H2.
+   apply (nat_case n1)
+    [intros.apply False_ind.apply (not_le_Sn_O ? H3)
+    |intros.simplify.
+     apply H
+      [
+       apply lt_S_S_to_lt.
+       assumption
+      |apply le_S_S_to_le.assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem lt_minus_r: \forall n,m,l:nat. 
+  n \le l \to l < m \to l -n < m -n.
+intro.elim n
+  [applyS H1
+  |rewrite > eq_minus_S_pred.
+   rewrite > eq_minus_S_pred.
+   apply lt_pred
+    [unfold lt.apply le_plus_to_minus_r.applyS H1
+    |apply H[autobatch|assumption]
+    ]
+  ]
+qed.
+
+lemma lt_to_lt_O_minus : \forall m,n.
+  n < m \to O < m - n.
+intros.  
+unfold. apply le_plus_to_minus_r. unfold in H. rewrite > sym_plus. 
+rewrite < plus_n_Sm. 
+rewrite < plus_n_O. 
+assumption.
+qed.  
+
 theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
 intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
 intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
@@ -236,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.