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