for a, b, n being Nat holds Lucas (a,b,1,(- 1),n) = GenFib (a,b,n) by Th8;