(* minus and lt - to be completed *)
theorem lt_minus_to_plus: \forall n,m,p. (lt n (p-m)) \to (lt (n+m) p).
-intros 3.apply nat_elim2 (\lambda m,p.(lt n (p-m)) \to (lt (n+m) p)).
+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.
+simplify.intros.apply False_ind.apply (not_le_Sn_O n H).
simplify.intros.
apply le_S_S.
rewrite < plus_n_Sm.