An efficient way to compute the fibonacci function

Here is a definition of the Fibonacci function.

Fixpoint fib (n:nat) : nat :=
  match n with
    0 => 1
  | 1 => 1
  | S ((S p) as q) => fib p + fib q
  end.

Prove the following statements:

  forall n, fib (2*n) = fib (n) * fib (n) + 
           (fib (n+1) - fib n)*(fib (n+1) - fib n).

  forall n, fib (2*n+1) = 2 * fib n * fib (n+1) - fib n * fib n.

  forall n, fib (S (2*n+1)) = fib (n+1) * (fib (n+1)) + fib n * fib n.

Use these formulas to define another function that computes the values of the Fibonacci function for n, with only a logarithmic number of recursive calls (to compute the values for 17 and 18, this function should only compute the values for 8, 9, 4, 5, 2, and 3).

Solution