case zero
n✝ n : ℕ
w : n ≠ 0
h : 1 < zero
⊢ digits zero n = n % zero :: digits zero (n / zero)

case succ.zero
n✝ n : ℕ
w : n ≠ 0
h : 1 < succ zero
⊢ digits (succ zero) n = n % succ zero :: digits (succ zero) (n / succ zero)

case succ.succ
n✝ n : ℕ
w : n ≠ 0
b : ℕ
h : 1 < succ (succ b)
⊢ digits (succ (succ b)) n = n % succ (succ b) :: digits (succ (succ b)) (n / succ (succ b))
n✝ b n : ℕ
h : 1 < b
w : n ≠ 0
⊢ digits b n = n % b :: digits b (n / b)
rcases b with (_ | _ | b)
case succ.succ.zero
n b : ℕ
h : 1 < succ (succ b)
w : zero ≠ 0
⊢ digits (succ (succ b)) zero = zero % succ (succ b) :: digits (succ (succ b)) (zero / succ (succ b))

case succ.succ.succ
n✝ b : ℕ
h : 1 < succ (succ b)
n : ℕ
w : succ n ≠ 0
⊢ digits (succ (succ b)) (succ n) = succ n % succ (succ b) :: digits (succ (succ b)) (succ n / succ (succ b))
case succ.succ
n✝ n : ℕ
w : n ≠ 0
b : ℕ
h : 1 < succ (succ b)
⊢ digits (succ (succ b)) n = n % succ (succ b) :: digits (succ (succ b)) (n / succ (succ b))
rcases n with (_ | n)
no goals
case succ.succ.succ
n✝ b : ℕ
h : 1 < succ (succ b)
n : ℕ
w : succ n ≠ 0
⊢ digits (succ (succ b)) (succ n) = succ n % succ (succ b) :: digits (succ (succ b)) (succ n / succ (succ b))
. simp only [digits_add_two_add_one, ne_eq]
no goals
case zero
n✝ n : ℕ
w : n ≠ 0
h : 1 < zero
⊢ digits zero n = n % zero :: digits zero (n / zero)
rw [digits_zero_succ' w, Nat.mod_zero, Nat.div_zero, Nat.digits_zero_zero]
no goals
case succ.zero
n✝ n : ℕ
w : n ≠ 0
h : 1 < succ zero
⊢ digits (succ zero) n = n % succ zero :: digits (succ zero) (n / succ zero)
norm_num at h
no goals
case succ.succ.zero
n b : ℕ
h : 1 < succ (succ b)
w : zero ≠ 0
⊢ digits (succ (succ b)) zero = zero % succ (succ b) :: digits (succ (succ b)) (zero / succ (succ b))
norm_num at w
no goals
case succ.succ.succ
n✝ b : ℕ
h : 1 < succ (succ b)
n : ℕ
w : succ n ≠ 0
⊢ digits (succ (succ b)) (succ n) = succ n % succ (succ b) :: digits (succ (succ b)) (succ n / succ (succ b))
simp only [digits_add_two_add_one, ne_eq]