apply (le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n)).
apply divides_to_max_prime_factor.
assumption.assumption.
apply (witness r n ((nth_prime p) \sup q)).
apply (le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n)).
apply divides_to_max_prime_factor.
assumption.assumption.
apply (witness r n ((nth_prime p) \sup q)).