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