theorem :: FIB_NUM3:46
for a, b, n being Element of NAT holds GenFib (b,(a + b),n) = GenFib (a,b,(n + 1))