apply le_S_S_to_le.assumption.
qed.
+(* ??? this needs not le *)
+theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
+intro.elim n.apply False_ind.exact not_le_Sn_O O H.
+apply eq_f.apply pred_Sn.
+qed.
+
(* le vs. lt *)
theorem lt_to_le : \forall n,m:nat. lt n m \to le n m.
simplify.intros.elim H.
intros 2.simplify.intro.elim H.
left.apply le_S_S.assumption.
right.intro.apply H1.apply le_S_S_to_le.assumption.
-qed.
-
-
+qed.
\ No newline at end of file