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