theorem :: FIB_NUM4:25

for n being Nat st n >= 2 holds
Fib (n + 1) = [/((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2)\]