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.
intros.
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.