theorem Th13: :: NUMBER03:13

for m, n being Nat st 0 < m holds
m gcd n <= m