have one_lt_ten : 1 < 10 := by norm_num
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
⊢ (Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * (x + 1))).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum
case succ
m y : ℕ
h1 : y < 10 ^ m
x : ℕ
h3 : (Nat.digits 10 y).length ≤ m
k : ℕ
hk : k + (Nat.digits 10 y).length = m
one_lt_ten : 1 < 10
⊢ (Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * (x + 1))).sum =
    (Nat.digits 10 ((x + 1) * 10 ^ m)).sum + (Nat.digits 10 y).sum