theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
intros.apply (lt_O_n_elim n H).intro.
apply (lt_O_n_elim m H1).intro.
-simplify.apply le_S_S.apply le_minus_m.
+simplify.unfold lt.apply le_S_S.apply le_minus_m.
qed.
theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
rewrite > plus_n_Sm.assumption.
qed.
+(* minus and lt - to be completed *)
+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.
+simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
+simplify.intros.unfold lt.
+apply le_S_S.
+rewrite < plus_n_Sm.
+apply H.apply H1.
+qed.
theorem distributive_times_minus: distributive nat times minus.
-simplify.
+unfold distributive.
intros.
apply ((leb_elim z y)).
intro.cut (x*(y-z)+x*z = (x*y-x*z)+x*z).
theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
\def distributive_times_minus.
+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.
+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).
intros.
cut (m+p \le n \or m+p \nleq n).