Disappearing base case

I like the Fibonacci sequence as an example for induction and recursion. It has an interesting structure, beginning with two base cases in its definition: F(0) = 0, F(1) = 1, and for n> 1, F(n) = F(n-2) + F(n-1).

The sequence is rich in properties. There are hundreds of connections between elements of the Fibonacci sequence. One such connection is that the sum of the Fibonacci numbers from 0 to n is F(n+2) - 1. Now here's where things take a strange turn.

The natural way to prove properties about a sequence defined recursively (read inductively) is using induction. To prove the above property, you need just one base case: the sum of the Fibonacci numbers from F(0) to F(0) is F(2) - 1 (check my calculation). The rest of the proof follows by simple induction. Assume that n is a generic natural number, and that the sum of the Fibonacci numbers from 0 to n is F(n+2)-1. Then the sum of the Fibonacci numbers from 0 to n+1 can be partitioned into the sum from 0 to n --- by assumption this is F(n+2) - 1 --- plus F(n+1). Adding these two terms yields F(n+3)-1, which verifies that the result for the Fibonacci numbers from 0 to n+1 follows from the result from 0 to n.

So, the result is true for every natural number n. Strange that when the definition of F(n) requires two base cases, proving this property requires just one.