(**************************************************************************)
-set "baseuri" "cic:/matita/nat/minus".
-
include "nat/le_arith.ma".
include "nat/compare.ma".
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.
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.
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.
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.