let n be Nat; :: thesis: Fib (n + 5) = (Fib (n + 3)) + (Fib (n + 4))
Fib (n + 5) = Fib (((n + 3) + 1) + 1)
.= (Fib (n + 3)) + (Fib ((n + 3) + 1)) by PRE_FF:1 ;
hence Fib (n + 5) = (Fib (n + 3)) + (Fib (n + 4)) ; :: thesis: verum