Verified solving and asymptotics of linear recurrences

Abstract

Linear recurrences with constant coefficients are an interesting class of recurrence equations that can be solved explicitly. The most famous example are certainly the Fibonacci numbers with the equation f(n) = f(n−1) + f(n−2) and the quite non-obvious closed form 1 √ 5 (ϕn − (−ϕ)−n) where ϕ is the golden ratio.