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