theorem :: FIB_NUM4:31

for n being Nat st n >= 2 holds
Lucas n = [/((tau to_power n) - (1 / 2))\]