for a, b, c being Integer st a,b are_coprime holds
c gcd (a * b) = (c gcd a) * (c gcd b)