theorem :: FIB_NUM4:36

for n being Nat st n <> 1 holds
Lucas (n + 1) = ((Lucas n) + (sqrt (5 * (((Lucas n) ^2) - (4 * ((- 1) to_power n)))))) / 2