theorem :: FIB_NUM4:34

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