for n being Nat holds Lucas (0,1,1,(- 1),n) = Fib n by Th6;