theorem :: FIB_NUM4:33

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