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