+(* 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))).
+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.unfold lt.
+apply le_S_S.
+rewrite < plus_n_Sm.
+apply H.apply H1.
+qed.