A tail recursive Fibonacci function

This exercise follows this one.
Define a tail-recursive (i.e. iterative) function that computes the n-th number of Fibonacci. You must prove that this new function and the one defined in this exercise compute exactly the same result.

Solution

Look at This file