let a, b, n be Element of NAT ; :: thesis: (GenFib (a,b,n)) + (GenFib (a,b,(n + 3))) = 2 * (GenFib (a,b,(n + 2)))

(GenFib (a,b,n)) + (GenFib (a,b,(n + 3))) = (GenFib (a,b,n)) + ((GenFib (a,b,(n + 1))) + (GenFib (a,b,(n + 2)))) by Th35

.= ((GenFib (a,b,n)) + (GenFib (a,b,(n + 1)))) + (GenFib (a,b,(n + 2)))

.= (GenFib (a,b,(n + 2))) + (GenFib (a,b,(n + 2))) by Th34

.= 2 * (GenFib (a,b,(n + 2))) ;

hence (GenFib (a,b,n)) + (GenFib (a,b,(n + 3))) = 2 * (GenFib (a,b,(n + 2))) ; :: thesis: verum

(GenFib (a,b,n)) + (GenFib (a,b,(n + 3))) = (GenFib (a,b,n)) + ((GenFib (a,b,(n + 1))) + (GenFib (a,b,(n + 2)))) by Th35

.= ((GenFib (a,b,n)) + (GenFib (a,b,(n + 1)))) + (GenFib (a,b,(n + 2)))

.= (GenFib (a,b,(n + 2))) + (GenFib (a,b,(n + 2))) by Th34

.= 2 * (GenFib (a,b,(n + 2))) ;

hence (GenFib (a,b,n)) + (GenFib (a,b,(n + 3))) = 2 * (GenFib (a,b,(n + 2))) ; :: thesis: verum