theorem :: FIB_NUM4:21

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