apply not_le_Sn_n.
qed.
+(*not lt*)
+theorem eq_to_not_lt: \forall a,b:nat.
+a = b \to a \nlt b.
+intros.
+unfold Not.
+intros.
+rewrite > H in H1.
+apply (lt_to_not_eq b b)
+[ assumption
+| reflexivity
+]
+qed.
+
(* le vs. lt *)
theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
simplify.intros.unfold lt in H.elim H.
theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
intro.elim n.reflexivity.
apply False_ind.
-apply not_le_Sn_O.
-goal 17. apply H1.
+apply not_le_Sn_O;
+[2: apply H1 | skip].
qed.
theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.