English
For b > 1 and any L, if w1 and w2 hold, then digits_b(ofDigits(b,L)) = L.
Русский
Для b > 1 и любого L, если соблюдены условия w1 и w2, то digits_b(ofDigits(b,L)) = L.
LaTeX
$$$1 < b \\Rightarrow (\\forall L)((\\forall \\ell \\in L, \\ell < b) \\Rightarrow ((L \\neq []) \\Rightarrow \\operatorname{digits}_b(\\operatorname{ofDigits}(b,L)) = L)).$$$
Lean4
theorem ofDigits_digits (b n : ℕ) : ofDigits b (digits b n) = n :=
by
rcases b with - | b
· rcases n with - | n
· rfl
· simp
· rcases b with - | b
·
induction n with
| zero => rfl
| succ n ih =>
rw [Nat.zero_add] at ih ⊢
simp only [ih, add_comm 1, ofDigits_one_cons, Nat.cast_id, digits_one_succ]
· induction n using Nat.strongRecOn with
| ind n h => ?_
cases n
· rw [digits_zero]
rfl
· simp only [digits_add_two_add_one]
dsimp [ofDigits]
rw [h _ (Nat.div_lt_self' _ b)]
rw [Nat.mod_add_div]
