(max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)).
(* max_prime_factor is indeed a factor *)
-theorem divides_max_prime_factor_n: \forall n:nat. (S O) < n \to
-nth_prime (max_prime_factor n) \divides n.
-intros.apply divides_b_true_to_divides.
-apply lt_O_nth_prime_n.
-apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n).
-cut (\exists i. nth_prime i = smallest_factor n).
-elim Hcut.
-apply (ex_intro nat ? a).
-split.
-apply (trans_le a (nth_prime a)).
-apply le_n_fn.
-exact lt_nth_prime_n_nth_prime_Sn.
-rewrite > H1. apply le_smallest_factor_n.
-rewrite > H1.
-change with (divides_b (smallest_factor n) n = true).
-apply divides_to_divides_b_true.
-apply (trans_lt ? (S O)).unfold lt. apply le_n.
-apply lt_SO_smallest_factor.assumption.
-apply divides_smallest_factor_n.
-apply (trans_lt ? (S O)). unfold lt. apply le_n. assumption.
-apply prime_to_nth_prime.
-apply prime_smallest_factor_n.assumption.
+theorem divides_max_prime_factor_n:
+ \forall n:nat. (S O) < n
+ \to nth_prime (max_prime_factor n) \divides n.
+intros; apply divides_b_true_to_divides;
+[ apply lt_O_nth_prime_n;
+| apply (f_max_true (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
+ cut (\exists i. nth_prime i = smallest_factor n);
+ [ elim Hcut.
+ apply (ex_intro nat ? a);
+ split;
+ [ apply (trans_le a (nth_prime a));
+ [ apply le_n_fn;
+ exact lt_nth_prime_n_nth_prime_Sn;
+ | rewrite > H1;
+ apply le_smallest_factor_n; ]
+ | rewrite > H1;
+ change with (divides_b (smallest_factor n) n = true);
+ apply divides_to_divides_b_true;
+ [ apply (trans_lt ? (S O));
+ [ unfold lt; apply le_n;
+ | apply lt_SO_smallest_factor; assumption; ]
+ | apply divides_smallest_factor_n;
+ apply (trans_lt ? (S O));
+ [ unfold lt; apply le_n;
+ | assumption; ] ] ]
+ | apply prime_to_nth_prime;
+ apply prime_smallest_factor_n;
+ assumption; ] ]
qed.
theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to