case zero
n b : ℕ
h : 2 ≤ b
w : 0 < zero
⊢ digitsAux b h zero = zero % b :: digitsAux b h (zero / b)

case succ
n b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < succ n✝
⊢ digitsAux b h (succ n✝) = succ n✝ % b :: digitsAux b h (succ n✝ / b)
n✝ b : ℕ
h : 2 ≤ b
n : ℕ
w : 0 < n
⊢ digitsAux b h n = n % b :: digitsAux b h (n / b)
cases n
no goals
case zero
n b : ℕ
h : 2 ≤ b
w : 0 < zero
⊢ digitsAux b h zero = zero % b :: digitsAux b h (zero / b)
cases w
no goals
case succ
n b : ℕ
h : 2 ≤ b
n✝ : ℕ
w : 0 < succ n✝
⊢ digitsAux b h (succ n✝) = succ n✝ % b :: digitsAux b h (succ n✝ / b)
rw [digitsAux]