Proof in Idris that exponential and linear time fib functions are equivalent

neilmitchell.blogspot.com