Fib 5 = Fib ((3 + 1) + 1)
.= (Fib 3) + (Fib (3 + 1)) by PRE_FF:1
.= 5 by FIB_NUM2:22, FIB_NUM2:23 ;
hence Fib 5 = 5 ; :: thesis: verum