English
The Zeckendorf representation of n is defined by zeckendorf(0)=[], and for n>0, zeckendorf(n) = greatestFib(n) :: zeckendorf(n - fib(greatestFib(n))).
Русский
Репрезентация Зекендорфа n задаётся так: zeckendorf(0)=[], для n>0: zeckendorf(n) = greatestFib(n) :: zeckendorf(n - fib(greatestFib(n))).
LaTeX
$$$$ \operatorname{zeckendorf}(0) = [] \quad\text{and}\quad \operatorname{zeckendorf}(n) = \operatorname{greatestFib}(n) :: \operatorname{zeckendorf}(n - \operatorname{fib}(\operatorname{greatestFib}(n))). $$$$
Lean4
/-- The Zeckendorf representation of a natural number.
Note: For unfolding, you should use the equational lemmas `Nat.zeckendorf_zero` and
`Nat.zeckendorf_of_pos` instead of the autogenerated one. -/
def zeckendorf : ℕ → List ℕ
| 0 => []
| m@(_ + 1) =>
letI a := greatestFib m
a :: zeckendorf (m - fib a)
decreasing_by simp_wf; subst_vars; apply zeckendorf_aux (zero_lt_succ _)
