An efficient Fibonacci function on binary numbers

This exercise follows this one.
Find a simple relation between (fib n, fib (n+1)) and (fib (2n), fib (2n+1)). Use this relation to construct an efficient function with the following type:

forall p:nat, {u:nat &{u':nat | u = fib n \coqand u' = fib(n+1)}}

using a recursive algorith on numbers of type positive.

Solution

Look at This file