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.
apply le_n_O_to_eq.apply le_S_S_to_le.exact H5.
simplify.intro.
cut O=n1.
-apply not_le_Sn_O O ?.
+apply not_le_Sn_O O.
rewrite > Hcut3 in \vdash (? ? %).
assumption.rewrite > Hcut.
rewrite < H6.reflexivity.
rewrite > Hcut3 in \vdash (? (? ? %)).
change with divides (nth_prime p) r \to False.
intro.
-apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r ? ? ? ?.
+apply plog_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r.
apply lt_SO_nth_prime_n.
simplify.apply le_S_S.apply le_O_n.apply le_n.
assumption.
elim Hcut3.absurd O=r.
apply le_n_O_to_eq.apply le_S_S_to_le.exact H2.
simplify.intro.
-apply not_le_Sn_O O ?.
+apply not_le_Sn_O O.
rewrite > H3 in \vdash (? ? %).assumption.assumption.
apply le_to_or_lt_eq r (S O).
apply not_lt_to_le.assumption.
cut i = j.
apply not_le_Sn_n i.rewrite > Hcut1 in \vdash (? ? %).assumption.
apply injective_nth_prime ? ? H4.
-apply H i (S j) ?.
+apply H i (S j).
apply trans_lt ? j.assumption.simplify.apply le_n.
assumption.
apply divides_times_to_divides.
rewrite > plus_n_O.
rewrite > plus_n_O (defactorize_aux n3 (S i)).assumption.
apply False_ind.
-apply not_divides_defactorize_aux n1 i (S i) ?.
+apply not_divides_defactorize_aux n1 i (S i).
simplify. apply le_n.
simplify in H5.
rewrite > plus_n_O (defactorize_aux n1 (S i)).
reflexivity.
intros.
apply False_ind.
-apply not_divides_defactorize_aux n3 i (S i) ?.
+apply not_divides_defactorize_aux n3 i (S i).
simplify. apply le_n.
simplify in H4.
rewrite > plus_n_O (defactorize_aux n3 (S i)).