theorem :: FIB_NUM4:38

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