theorem :: FIB_NUM:8

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