for a, b being Integer holds |.(a * b).| = (a gcd b) * (a lcm b)