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