theorem :: FIB_NUM4:35

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