theorem :: FIB_NUM:8

for n being Nat holds |.((Fib n) - ((tau to_power n) / (sqrt 5))).| < 1