induction' m with m ih
b m : ℕ
⊢ Nat.ofDigits b (List.replicate m 0) = 0
case zero
b : ℕ
⊢ Nat.ofDigits b (List.replicate 0 0) = 0

case succ
b m : ℕ
ih : Nat.ofDigits b (List.replicate m 0) = 0
⊢ Nat.ofDigits b (List.replicate (m + 1) 0) = 0