let a, b, n be Nat; :: thesis: (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) = GenFib (a,b,(n + 2))
(GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) = GenFib (a,b,((n + 1) + 1)) by Th32
.= GenFib (a,b,(n + 2)) ;
hence (GenFib (a,b,n)) + (GenFib (a,b,(n + 1))) = GenFib (a,b,(n + 2)) ; :: thesis: verum