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

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