intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
intros 3.apply (nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p))).
intro.rewrite < plus_n_O.rewrite < minus_n_O.intro.assumption.
simplify.intros.apply False_ind.apply (not_le_Sn_O n H).