English
Let b, f, n, e be natural numbers with e > 0. If n < b^e, then the length of Nat.toDigitsCore b f n [] is at most e.
Русский
Пусть b, f, n, e — натуральные числа, e > 0. Если n < b^e, то длина Nat.toDigitsCore b f n [] не превосходит e.
LaTeX
$$$\\forall b,f,n,e \\in \\mathbb{N},\\ 0 < e \\land n < b^{e} \\Rightarrow |\\mathrm{Nat.toDigitsCore}\\,b\\,f\\,n\\,[]| \\le e$$$
Lean4
/-- The String representation produced by toDigitsCore has the proper length relative to
the number of digits in `n < e` for some base `b`. Since this works with any base,
it can be used for binary, decimal, and hex. -/
theorem toDigitsCore_length (b f n e : Nat) (h_e_pos : 0 < e) (hlt : n < b ^ e) :
(Nat.toDigitsCore b f n []).length ≤ e := by
induction f generalizing n e hlt h_e_pos with
| zero => simp only [toDigitsCore, List.length, zero_le]
| succ f ih =>
simp only [toDigitsCore]
cases e with
| zero => exact False.elim (Nat.lt_irrefl 0 h_e_pos)
| succ e =>
cases e with
| zero =>
rw [zero_add, pow_one] at hlt
simp [Nat.div_eq_of_lt hlt]
| succ e =>
specialize ih (n / b) _ (add_one_pos e) (Nat.div_lt_of_lt_mul <| by rwa [← pow_add_one'])
split_ifs
· simp only [List.length_singleton, _root_.zero_le, succ_le_succ]
· simp only [toDigitsCore_lens_eq b f (n / b) (Nat.digitChar <| n % b), Nat.succ_le_succ_iff, ih]
