theorem Th1: :: FIB_NUM:1

for m, n being Element of NAT holds m gcd n = m gcd (n + m)