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