English
Let b > 1, and x,y with x < b and not both zero. Then digits(b, x + b y) equals the list with head x followed by digits(b, y).
Русский
Пусть b > 1, и x,y такие, что x < b и не оба равны нулю. Тогда digits_b(x + b y) = [x] \u2227 digits_b(y).
LaTeX
$$$\\forall b>1\\forall x\\forall y\\;\\bigl(x < b\\bigr) \\Rightarrow (x \\neq 0 \\lor y \\neq 0) \\Rightarrow \\operatorname{digits}_b(x + b y) = x \\\\: \\;::\\; \\operatorname{digits}_b(y).$$$
Lean4
theorem digits_add (b : ℕ) (h : 1 < b) (x y : ℕ) (hxb : x < b) (hxy : x ≠ 0 ∨ y ≠ 0) :
digits b (x + b * y) = x :: digits b y :=
by
rcases Nat.exists_eq_add_of_le' h with ⟨b, rfl : _ = _ + 2⟩
cases y
· simp [hxb, hxy.resolve_right (absurd rfl)]
dsimp [digits]
rw [digitsAux_def]
· congr
· simp [Nat.add_mod, mod_eq_of_lt hxb]
· simp [add_mul_div_left, div_eq_of_lt hxb]
· apply Nat.succ_pos
