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