let n be Element of NAT ; :: thesis: (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2))

A1: 2 * (GenFib (2,1,(n + 2))) = 2 * (Lucas (n + 2)) by Th38;

( GenFib (2,1,n) = Lucas n & GenFib (2,1,(n + 3)) = Lucas (n + 3) ) by Th38;

hence (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2)) by A1, Th39; :: thesis: verum

A1: 2 * (GenFib (2,1,(n + 2))) = 2 * (Lucas (n + 2)) by Th38;

( GenFib (2,1,n) = Lucas n & GenFib (2,1,(n + 3)) = Lucas (n + 3) ) by Th38;

hence (Lucas n) + (Lucas (n + 3)) = 2 * (Lucas (n + 2)) by A1, Th39; :: thesis: verum