change with (smallest_factor (S n!) \le n \to False).intro.
apply (not_divides_S_fact n (smallest_factor(S n!))).
apply lt_SO_smallest_factor.
-simplify.apply le_S_S.apply le_SO_fact.
+unfold lt.apply le_S_S.apply le_SO_fact.
assumption.
apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
+unfold lt.apply le_S_S.apply le_O_n.
qed.
theorem ex_prime: \forall n. (S O) \le n \to \exists m.
apply prime_smallest_factor_n.
change with ((S(S O)) \le S (S n1)!).
apply le_S.apply le_SSO_fact.
-simplify.apply le_S_S.assumption.
+unfold lt.apply le_S_S.assumption.
qed.
let rec nth_prime n \def
qed.
theorem lt_SO_nth_prime_n : \forall n:nat. (S O) \lt nth_prime n.
-intros. elim n.simplify.apply le_n.
+intros. elim n.unfold lt.apply le_n.
apply (trans_lt ? (nth_prime n1)).
assumption.apply lt_nth_prime_n_nth_prime_Sn.
qed.
theorem lt_O_nth_prime_n : \forall n:nat. O \lt nth_prime n.
intros.apply (trans_lt O (S O)).
-simplify. apply le_n.apply lt_SO_nth_prime_n.
+unfold lt. apply le_n.apply lt_SO_nth_prime_n.
qed.
theorem ex_m_le_n_nth_prime_m:
apply (ex_intro nat ? a).assumption.
apply le_to_or_lt_eq.assumption.
apply ex_m_le_n_nth_prime_m.
-simplify.simplify in H.elim H.assumption.
+simplify.unfold prime in H.elim H.assumption.
qed.