intros.apply divides_b_true_to_divides.
apply lt_O_nth_prime_n.
apply f_max_true (\lambda p:nat.eqb (mod n (nth_prime p)) O) n.
-cut ex nat (\lambda i. nth_prime i = smallest_factor n).
+cut \exists i. nth_prime i = smallest_factor n.
elim Hcut.
apply ex_intro nat ? a.
split.