theorem :: FIB_NUM4:19

for n being Nat st n <> 0 holds
[/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n