cases' n with n
n : ℕ
hn : 0 < n
⊢ (10 ^ (Nat.digits 10 n).length + n) / 10 = 10 ^ (Nat.digits 10 (n / 10)).length + n / 10
case zero
hn : 0 < 0
⊢ (10 ^ (Nat.digits 10 0).length + 0) / 10 = 10 ^ (Nat.digits 10 (0 / 10)).length + 0 / 10

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