English
For every n, zeckendorf(n) is a Zeckendorf representation: (zeckendorf(n)).IsZeckendorfRep.
Русский
Для каждого n представление zeckendorf(n) является репрезентацией Зекендорфа: (zeckendorf(n)).IsZeckendorfRep.
LaTeX
$$$$ \operatorname{IsZeckendorfRep}(\operatorname{zeckendorf}(n)). $$$$
Lean4
theorem isZeckendorfRep_zeckendorf : ∀ n, (zeckendorf n).IsZeckendorfRep
| 0 => by simp only [zeckendorf_zero, IsZeckendorfRep_nil]
| n + 1 => by
rw [zeckendorf_succ, IsZeckendorfRep, List.cons_append]
refine (isZeckendorfRep_zeckendorf _).cons' (fun a ha ↦ ?_)
obtain h | h := eq_zero_or_pos (n + 1 - fib (greatestFib (n + 1)))
· simp only [h, zeckendorf_zero, nil_append, head?_cons, Option.mem_some_iff] at ha
subst ha
exact le_greatestFib.2 le_add_self
rw [zeckendorf_of_pos h, cons_append, head?_cons, Option.mem_some_iff] at ha
subst a
exact
add_le_of_le_tsub_right_of_le (le_greatestFib.2 le_add_self)
(greatestFib_sub_fib_greatestFib_le_greatestFib n.succ_ne_zero)
