English
For base b and n, if n>0 and n<b, then digits b n = [n] and 1<b and 0<n.
Русский
Для основания b и n: если n>0 и n<b, то digits b n = [n] и 1<b и 0<n.
LaTeX
$$$\\forall b\\; n,\\ n>0 \\land n < b \\Rightarrow Nat.digits\\ b\\ n = [n] \\land 1 < b \\land 0 < n$$$
Lean4
theorem digits_append_digits {b m n : ℕ} (hb : 0 < b) :
digits b n ++ digits b m = digits b (n + b ^ (digits b n).length * m) :=
by
rcases eq_or_lt_of_le (Nat.succ_le_of_lt hb) with (rfl | hb)
· simp
rw [← ofDigits_digits_append_digits]
refine (digits_ofDigits b hb _ (fun l hl => ?_) (fun h_append => ?_)).symm
· rcases (List.mem_append.mp hl) with (h | h) <;> exact digits_lt_base hb h
· by_cases h : digits b m = []
· simp only [h, List.append_nil] at h_append ⊢
exact getLast_digit_ne_zero b <| digits_ne_nil_iff_ne_zero.mp h_append
· exact (List.getLast_append_of_right_ne_nil _ _ h) ▸ (getLast_digit_ne_zero _ <| digits_ne_nil_iff_ne_zero.mp h)
