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