#
An efficient Fibonacci function on binary numbers

This exercise follows this one.

Find a simple relation between `(fib `*n*, fib (*n*+1))
and `(fib (2`*n*), fib (2*n*+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

Going home

Pierre Castéran