theorem Th1: :: FIB_NUM:1
for m, n being Element of NAT holds m gcd n = m gcd (n + m)