theorem Th1: :: FIB_NUM:1

for m, n being Nat holds m gcd n = m gcd (n + m)