+theorem lt_pred: \forall n,m.
+ O < n \to n < m \to pred n < pred m.
+apply nat_elim2
+ [intros.apply False_ind.apply (not_le_Sn_O ? H)
+ |intros.apply False_ind.apply (not_le_Sn_O ? H1)
+ |intros.simplify.unfold.apply le_S_S_to_le.assumption
+ ]
+qed.
+