English
For base b>0 and digits of n, digits of n appended with digits of m equals digits of a shifted sum: n + b^{|digits n|} * m.
Русский
Для основания b>0 и цифр n, при добавлении цифр m: digits b n ++ digits b m = digits b (n + b^{|digits b n|} * m).
LaTeX
$$$\\forall {b m n : \\mathbb{N}}\\ (hb:\\ 0 < b) \\Rightarrow \n digits\\ b\\ n ++ digits\\ b\\ m = digits\\ b\\ (n + b ^ (digits\\ b\\ n).length * m)$$$
Lean4
theorem getLast_digit_ne_zero (b : ℕ) {m : ℕ} (hm : m ≠ 0) :
(digits b m).getLast (digits_ne_nil_iff_ne_zero.mpr hm) ≠ 0 :=
by
rcases b with (_ | _ | b)
· cases m
· cases hm rfl
· simp
· cases m
· cases hm rfl
simp only [zero_add, digits_one, List.getLast_replicate_succ]
exact Nat.one_ne_zero
revert hm
induction m using Nat.strongRecOn with
| ind n IH => ?_
intro hn
by_cases hnb : n < b + 2
· simpa only [digits_of_lt (b + 2) n hn hnb]
· rw [digits_getLast n (le_add_left 2 b)]
refine IH _ (Nat.div_lt_self hn.bot_lt (one_lt_succ_succ b)) ?_
rw [← pos_iff_ne_zero]
exact Nat.div_pos (le_of_not_gt hnb) (zero_lt_succ (succ b))
