cases' x with x
m x : ℕ
⊢ (Nat.digits 10 (x * 10 ^ m)).sum = (Nat.digits 10 x).sum
case zero
m : ℕ
⊢ (Nat.digits 10 (0 * 10 ^ m)).sum = (Nat.digits 10 0).sum

case succ
m x : ℕ
⊢ (Nat.digits 10 ((x + 1) * 10 ^ m)).sum = (Nat.digits 10 (x + 1)).sum