(**************************************************************************)
-set "baseuri" "cic:/matita/nat/minus".
-
include "nat/le_arith.ma".
include "nat/compare.ma".
[O \Rightarrow (S p)
| (S q) \Rightarrow minus p q ]].
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
+interpretation "natural minus" 'minus x y = (minus x y).
theorem minus_n_O: \forall n:nat.n=n-O.
intros.elim n.simplify.reflexivity.
theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
intros 2.
-generalize in match n.
-elim m.
+elim m in n ⊢ %.
rewrite < minus_n_O.apply plus_n_O.
-elim n2.simplify.
+elim n1.simplify.
apply minus_n_n.
rewrite < plus_n_Sm.
-change with (S n3 = (S n3 + n1)-n1).
+change with (S n2 = (S n2 + n)-n).
apply H.
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.
+unfold. apply le_plus_to_minus_r. unfold in H.
+cut ((S n ≤ m) = (1 + n ≤ m)) as applyS;
+ [ rewrite < applyS; assumption;
+ | demodulate; reflexivity. ]
+(*
+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).
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.
theorem eq_minus_plus_plus_minus: \forall n,m,p:nat. p \le m \to (n+m)-p = n+(m-p).
intros.
apply plus_to_minus.
+lapply (plus_minus_m_m ?? H); demodulate. reflexivity.
+(*
rewrite > sym_plus in \vdash (? ? ? %).
rewrite > assoc_plus.
rewrite < plus_minus_m_m.
reflexivity.assumption.
+*)
qed.
theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).