theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
n = m+p.
-intros.apply trans_eq ? ? ((n-m)+m) ?.
+intros.apply trans_eq ? ? ((n-m)+m).
apply plus_minus_m_m.
apply H.elim H1.
apply sym_plus.
apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
intros.simplify.reflexivity.
intros.apply False_ind.
-(* ancora problemi con il not *)
-apply not_le_Sn_O n1 H.
+apply not_le_Sn_O.
+goal 13.apply H.
intros.
simplify.apply H.apply le_S_S_to_le. apply H1.
qed.
intros.simplify.apply le_S.assumption.
qed.
+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.
+qed.
+
theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
intros 2.
apply nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m).
theorem distributive_times_minus: distributive nat times minus.
simplify.
intros.
-apply (leb_elim z y).intro.
-cut x*(y-z)+x*z = (x*y-x*z)+x*z.
-apply inj_plus_l (x*z).
-assumption.
-apply trans_eq nat ? (x*y).
-rewrite < distr_times_plus.
-rewrite < plus_minus_m_m ? ? H.reflexivity.
-rewrite < plus_minus_m_m ? ? ?.reflexivity.
-apply le_times_r.
-assumption.
-intro.
-rewrite > eq_minus_n_m_O.
-rewrite > eq_minus_n_m_O (x*y).
-rewrite < sym_times.simplify.reflexivity.
-apply lt_to_le.
-apply not_le_to_lt.assumption.
-apply le_times_r.apply lt_to_le.
-apply not_le_to_lt.assumption.
+apply (leb_elim z y).
+ intro.cut x*(y-z)+x*z = (x*y-x*z)+x*z.
+ apply inj_plus_l (x*z).assumption.
+ apply trans_eq nat ? (x*y).
+ rewrite < distr_times_plus.rewrite < plus_minus_m_m ? ? H.reflexivity.
+ rewrite < plus_minus_m_m.
+ reflexivity.
+ apply le_times_r.assumption.
+ intro.rewrite > eq_minus_n_m_O.
+ rewrite > eq_minus_n_m_O (x*y).
+ rewrite < sym_times.simplify.reflexivity.
+ apply le_times_r.apply lt_to_le.apply not_le_to_lt.assumption.
+ apply lt_to_le.apply not_le_to_lt.assumption.
qed.
theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
\def distributive_times_minus.
+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.
+ elim Hcut.
+ symmetry.apply plus_to_minus.assumption.
+ rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
+ rewrite > sym_plus.rewrite < plus_minus_m_m.
+ reflexivity.
+ apply trans_le ? (m+p).
+ rewrite < sym_plus.apply le_plus_n.
+ assumption.
+ apply le_plus_to_minus_r.rewrite > sym_plus.assumption.
+ rewrite > eq_minus_n_m_O n (m+p).
+ rewrite > eq_minus_n_m_O (n-m) p.
+ reflexivity.
+ apply le_plus_to_minus.apply lt_to_le. rewrite < sym_plus.
+ apply not_le_to_lt. assumption.
+ apply lt_to_le.apply not_le_to_lt.assumption.
+ apply decidable_le (m+p) n.
+qed.
+
+theorem eq_plus_minus_minus_minus: \forall n,m,p:nat. p \le m \to m \le n \to
+p+(n-m) = n-(m-p).
+intros.
+apply sym_eq.
+apply plus_to_minus.
+apply le_plus_to_minus.
+apply trans_le ? n.assumption.rewrite < sym_plus.apply le_plus_n.
+rewrite < assoc_plus.
+rewrite < plus_minus_m_m.
+rewrite < sym_plus.
+rewrite < plus_minus_m_m.reflexivity.
+assumption.assumption.
+qed.