rw [List.sum_cons, zero_add]
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ (0 :: Nat.digits 10 ((x + 1) * 10 ^ m * 10 / 10)).sum = (Nat.digits 10 (x + 1)).sum
case succ.succ
x m : ℕ
ih : (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m * 10 / 10)).sum = (Nat.digits 10 (x + 1)).sum