English
Let b, f, n, e be natural numbers with 0 < e and n < b^e. Then the length of (Nat.toDigits b f n) is at most e.
Русский
Пусть b, f, n, e — натуральные числа, 0 < e и n < b^e. Тогда длина (Nat.toDigits b f n) не превосходит e.
LaTeX
$$$\\forall b,f,n,e \\in \\mathbb{N},\\ 0 < e \\land n < b^{e} \\Rightarrow |\\mathrm{Nat.toDigits}\\,b\\,f\\,n| \\le e$$$
Lean4
/-- The core implementation of `Nat.toDigits` returns a String with length less than or equal to the
number of digits in the base-`b` number (represented by `e`). For example, the string
representation of any number less than `b ^ 3` has a length less than or equal to 3. -/
theorem toDigits_length (b n e : Nat) : 0 < e → n < b ^ e → (Nat.toDigits b n).length ≤ e :=
toDigitsCore_length _ _ _ _
