let n be Nat; :: thesis: Fib (n + 1) = (Fib (n + 2)) - (Fib n)
(Fib (n + 2)) - (Fib n) = (Fib ((n + 1) + 1)) - (Fib n)
.= ((Fib n) + (Fib (n + 1))) - (Fib n) by PRE_FF:1
.= Fib (n + 1) ;
hence Fib (n + 1) = (Fib (n + 2)) - (Fib n) ; :: thesis: verum