theorem Th22: :: FIB_NUM4:22

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