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