theorem :: FIB_NUM4:30

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