theorem Th53: :: NEWTON:53

for n, m being Nat holds (m gcd n) lcm n = n