rw [Nat.add_mul_div_left _ _ (Nat.succ_pos 9)]
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1 + 10 * 10 ^ (Nat.digits 10 (n.succ / 10)).length) / 10 =
    10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10
case succ
n : ℕ
hn : 0 < n + 1
⊢ (n + 1) / Nat.succ 9 + 10 ^ (Nat.digits 10 (n.succ / 10)).length =
    10 ^ (Nat.digits 10 ((n + 1) / 10)).length + (n + 1) / 10