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.
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.
apply prime_smallest_factor_n.
change with ((S(S O)) \le S (S n1)!).
apply le_S.apply le_SSO_fact.
apply prime_smallest_factor_n.
change with ((S(S O)) \le S (S n1)!).
apply le_S.apply le_SSO_fact.
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)).
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)).
apply (ex_intro nat ? a).assumption.
apply le_to_or_lt_eq.assumption.
apply 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.