English
If b > 1, L is a list of digits with each element less than b and the last element nonzero, then digits_b(ofDigits(b,L)) = L.
Русский
Если b>1, L — список цифр все элементы которого меньше b и последний не ноль, тогда digits_b(ofDigits(b,L)) = L.
LaTeX
$$$1 < b \\land (\\forall \\ell \\in L, \\ell < b) \\land (L \\neq []) \\Rightarrow \\operatorname{digits}_b(\\operatorname{ofDigits}(b,L)) = L.$$$
Lean4
theorem digits_ofDigits (b : ℕ) (h : 1 < b) (L : List ℕ) (w₁ : ∀ l ∈ L, l < b) (w₂ : ∀ h : L ≠ [], L.getLast h ≠ 0) :
digits b (ofDigits b L) = L := by
induction L with
| nil => simp
| cons d L ih =>
dsimp [ofDigits]
replace w₂ := w₂ (by simp)
rw [digits_add b h]
· rw [ih]
· intro l m
apply w₁
exact List.mem_cons_of_mem _ m
· intro h
rw [List.getLast_cons h] at w₂
convert w₂
· exact w₁ d List.mem_cons_self
· by_cases h' : L = []
· rcases h' with rfl
left
simpa using w₂
· right
contrapose! w₂
refine digits_zero_of_eq_zero h.ne_bot w₂ _ ?_
rw [List.getLast_cons h']
exact List.getLast_mem h'
