theorem :: FIB_NUM4:18

for n being Nat holds [\(((tau to_power n) / (sqrt 5)) + (1 / 2))/] = Fib n