case intro
n b x : ℕ
hx : succ x ≠ 0
hxb : succ x < b
⊢ digits b (succ x) = [succ x]
n b x : ℕ
hx : x ≠ 0
hxb : x < b
⊢ digits b x = [x]
rcases exists_eq_succ_of_ne_zero hx with ⟨x, rfl⟩
case intro.intro
n x : ℕ
hx : succ x ≠ 0
b : ℕ
hxb : succ x < b + succ 1
⊢ digits (b + succ 1) (succ x) = [succ x]
case intro
n b x : ℕ
hx : succ x ≠ 0
hxb : succ x < b
⊢ digits b (succ x) = [succ x]
rcases exists_eq_add_of_le' ((Nat.le_add_left 1 x).trans_lt hxb) with ⟨b, rfl⟩
no goals
case intro.intro
n x : ℕ
hx : succ x ≠ 0
b : ℕ
hxb : succ x < b + succ 1
⊢ digits (b + succ 1) (succ x) = [succ x]
rw [digits_add_two_add_one, div_eq_of_lt hxb, digits_zero, mod_eq_of_lt hxb]