+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).
+ elim Hcut.
+ 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.
+ 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.
+rewrite < assoc_plus.
+rewrite < plus_minus_m_m.
+rewrite < sym_plus.
+rewrite < plus_minus_m_m.reflexivity.
+assumption.assumption.
+qed.