theorem Th23: :: FIB_NUM3:23

for n being Nat holds (Lucas (n + 3)) - (2 * (Lucas n)) = 5 * (Fib n)