ring
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
h5 :
  Nat.digits 10 y ++ List.replicate k 0 ++ Nat.digits 10 x.succ =
    Nat.digits 10 (y + 10 ^ (k + (Nat.digits 10 y).length) * x.succ)
⊢ (Nat.digits 10 y).sum + (Nat.digits 10 x.succ).sum = (Nat.digits 10 (x + 1)).sum + (Nat.digits 10 y).sum
no goals