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.
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.