theorem Th28: :: NAT_D:28

for m, n being natural Number st m > 0 holds
n gcd m = m gcd (n mod m)