rw [Nat.digits_def' (by norm_num) hyp]
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (Nat.digits 10 y).length < m + 1 + 1
case succ.inr
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
hyp : y > 0
⊢ (y % 10 :: Nat.digits 10 (y / 10)).length < m + 1 + 1