apply divides_gcd_n.
apply divides_times_to_divides.
apply prime_smallest_factor_n.
assumption.
apply (transitive_divides ? (gcd m (n*p))).
apply divides_smallest_factor_n.
apply divides_gcd_n.
apply divides_times_to_divides.
apply prime_smallest_factor_n.
assumption.
apply (transitive_divides ? (gcd m (n*p))).
apply divides_smallest_factor_n.