theorem :: FIB_NUM2:1

for n being non zero Element of NAT holds (n -' 1) + 2 = n + 1