theorem :: FIB_NUM4:32

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