theorem :: FIB_NUM:5

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