theorem :: NEWTON06:44

for a, b, c, d being Nat st a,b are_coprime & a * b = c * d holds
a * b = (((a gcd c) * (b gcd c)) * (a gcd d)) * (b gcd d)