for m being Nat holds m gcd 1 = 1