English
If n = r + b*m with r < b and (digits b m) = l and 1 < b and 0 < m, then digits b n = r :: l, with 1 < b and 0 < n.
Русский
Если n = r + b m с r < b и digits b m = l и 1 < b и 0 < m, то digits b n = r :: l, и 1 < b, 0 < n.
LaTeX
$$$\\forall b,n,m,r,l\\; (e:\\ r + b \\cdot m = n)\\; (hr: r < b)\\; (h: Nat.digits\\; b\\; m = l \\land 1 < b \\land 0 < m) \\Rightarrow (Nat.digits\\; b\\; n = r :: l) \\land 1 < b \\land 0 < n$$$
Lean4
theorem digits_succ (b n m r l) (e : r + b * m = n) (hr : r < b) (h : Nat.digits b m = l ∧ 1 < b ∧ 0 < m) :
(Nat.digits b n = r :: l) ∧ 1 < b ∧ 0 < n :=
by
rcases h with ⟨h, b2, m0⟩
have b0 : 0 < b := by omega
have n0 : 0 < n := by linarith [mul_pos b0 m0]
refine ⟨?_, b2, n0⟩
obtain ⟨rfl, rfl⟩ := (Nat.div_mod_unique b0).2 ⟨e, hr⟩
subst h; exact Nat.digits_def' b2 n0
