theorem Th1: :: NUMBER07:1

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