intros.simplify.apply H.apply le_S_S_to_le.assumption.
qed.
+theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
+intros 2.
+generalize in match n.
+elim m.
+rewrite < minus_n_O.apply plus_n_O.
+elim n2.simplify.
+apply minus_n_n.
+rewrite < plus_n_Sm.
+change with S n3 = (S n3 + n1)-n1.
+apply H.
+qed.
+
theorem plus_minus_m_m: \forall n,m:nat.
m \leq n \to n = (n-m)+m.
intros 2.
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.
qed.
-theorem plus_to_minus :\forall n,m,p:nat.m \leq n \to
+theorem plus_to_minus :\forall n,m,p:nat.
n = m+p \to n-m = p.
intros.
apply inj_plus_r m.
-rewrite < H1.
+rewrite < H.
rewrite < sym_plus.
symmetry.
-apply plus_minus_m_m.assumption.
+apply plus_minus_m_m.rewrite > H.
+rewrite > sym_plus.
+apply le_plus_n.
qed.
theorem minus_S_S : \forall n,m:nat.
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.
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 ? ? ?.
+ rewrite < plus_minus_m_m.
reflexivity.
apply le_times_r.assumption.
intro.rewrite > eq_minus_n_m_O.
theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
intros.
-cut m+p \le n \or \not m+p \le n.
+cut m+p \le n \or m+p \nleq n.
elim Hcut.
- symmetry.apply plus_to_minus.assumption.
+ symmetry.apply plus_to_minus.
rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
rewrite > sym_plus.rewrite < plus_minus_m_m.
reflexivity.
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.