English
Let l be a nonempty list of natural numbers with last element nonzero, and let b be a natural number. If we set a = b + 2, then a^{|l|} ≤ a · ofDigits(a, l).
Русский
Пусть l — непустой список натуральных чисел и последнее число списка не равно нулю. Положим a = b + 2. Тогда a^{|l|} ≤ a · ofDigits(a, l).
LaTeX
$$$ (b+2)^{|l|} \le (b+2) \cdot \operatorname{ofDigits}(b+2, l) $$$
Lean4
theorem pow_length_le_mul_ofDigits {b : ℕ} {l : List ℕ} (hl : l ≠ []) (hl2 : l.getLast hl ≠ 0) :
(b + 2) ^ l.length ≤ (b + 2) * ofDigits (b + 2) l :=
by
rw [← List.dropLast_append_getLast hl]
simp only [List.length_append, List.length, zero_add, List.length_dropLast, ofDigits_append, List.length_dropLast,
ofDigits_singleton, add_comm (l.length - 1), pow_add, pow_one]
apply Nat.mul_le_mul_left
refine le_trans ?_ (Nat.le_add_left _ _)
have : 0 < l.getLast hl := by rwa [pos_iff_ne_zero]
convert Nat.mul_le_mul_left ((b + 2) ^ (l.length - 1)) this using 1
rw [Nat.mul_one]
