nat.prod_dvd_and_dvd_of_dvd_prod
Represent a divisor of
m
*
n
as a product of a divisor of
m
and a divisor of
n
.