theorem Th23: :: FIB_NUM4:23

for n being Nat st n >= 2 & n is odd holds
Fib (n + 1) = [/((tau * (Fib n)) - 1)\]