English
If l is a Zeckendorf representation and every element of l is less than n, then the sum of fib numbers in l is less than fib(n).
Русский
Если l — репрезентация Зекендорфа и все элементы l меньше n, тогда сумма fib чисел в l меньше fib(n).
LaTeX
$$$$ (l \text{ IsZeckendorfRep}) \Rightarrow (\forall a \in l, a < n) \Rightarrow \bigl(\sum_{x \in l} \operatorname{fib}(x)\bigr) < \operatorname{fib}(n). $$$$
Lean4
theorem sum_fib_lt : ∀ {n l}, IsZeckendorfRep l → (∀ a ∈ (l ++ [0]).head?, a < n) → (l.map fib).sum < fib n
| _, [], _, hn => fib_pos.2 <| hn _ rfl
| n, a :: l, hl, hn =>
by
simp only [IsZeckendorfRep, cons_append, isChain_iff_pairwise, pairwise_cons] at hl
have : ∀ b, b ∈ head? (l ++ [0]) → b < a - 1 := fun b hb ↦ lt_tsub_iff_right.2 <| hl.1 _ <| mem_of_mem_head? hb
simp only [mem_append, mem_singleton, ← isChain_iff_pairwise, or_imp, forall_and, forall_eq, zero_add] at hl
simp only [map, List.sum_cons]
refine (add_lt_add_left (sum_fib_lt hl.2 this) _).trans_le ?_
rw [add_comm, ← fib_add_one (hl.1.2.trans_lt' zero_lt_two).ne']
exact fib_mono (hn _ rfl)
