theorem Th96: :: PREPOWER:96

for m, n being Nat holds m gcd n = m gcd |.(n - m).|