theorem GL: :: NEWTON03:69

for a, b being non zero Nat holds a / (a gcd b) = (a lcm b) / b