rw [Nat.digits_def' two_le_ten hn, List.length]
n : ℕ
hn : 0 < n
⊢ (Nat.digits 10 n).length = 1 + (Nat.digits 10 (n / 10)).length
n : ℕ
hn : 0 < n
⊢ (Nat.digits 10 (n / 10)).length + 1 = 1 + (Nat.digits 10 (n / 10)).length