let a, b, n be Element of NAT ; :: thesis: (GenFib (a,b,n)) + (GenFib (a,b,(n + 4))) = 3 * (GenFib (a,b,(n + 2)))
(GenFib (a,b,n)) + (GenFib (a,b,(n + 4))) = (GenFib (a,b,n)) + ((GenFib (a,b,(n + 2))) + (GenFib (a,b,(n + 3)))) by Th36
.= ((GenFib (a,b,n)) + (GenFib (a,b,(n + 2)))) + (GenFib (a,b,(n + 3)))
.= ((GenFib (a,b,n)) + (GenFib (a,b,(n + 2)))) + ((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))) + (GenFib (a,b,(n + 2)))) + (GenFib (a,b,(n + 2))) by Th34
.= 3 * (GenFib (a,b,(n + 2))) ;
hence (GenFib (a,b,n)) + (GenFib (a,b,(n + 4))) = 3 * (GenFib (a,b,(n + 2))) ; :: thesis: verum