-cut m+p \le n \or \not m+p \le n.
-elim Hcut.
-apply sym_eq.
-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.
-rewrite > eq_minus_n_m_O n (m+p).
-rewrite > eq_minus_n_m_O (n-m) p.reflexivity.
-apply decidable_le (m+p) n.
-apply le_plus_to_minus_r.
-rewrite > sym_plus.assumption.
-apply trans_le ? (m+p).
-rewrite < sym_plus.
-apply le_plus_n.assumption.
-apply lt_to_le.apply not_le_to_lt.assumption.
-apply le_plus_to_minus.
-apply lt_to_le.apply not_le_to_lt.
-rewrite < sym_plus.assumption.
+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.