Zeckendorf’s Theorem

This work formalizes Zeckendorf's theorem. The theorem states that every positive integer can be uniquely represented as a sum of one or more non-consecutive Fibonacci numbers. More precisely, if $N$ is a positive integer, there exist unique positive integers $c_i\ge 2$ with $c_{i+1}>c_i+1$, such that $$N=\sum _{i=0}^k{F}_{c_i}$$ where $F_n$ is the $n$-th Fibonacci number.