obtain rfl | hyp := Nat.eq_zero_or_pos y
case succ
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
y : ℕ
hy : y < 10 ^ (m + 1)
⊢ (Nat.digits 10 y).length < m + 1 + 1
case succ.inl
m : ℕ
ih : ∀ {y : ℕ}, y < 10 ^ m → (Nat.digits 10 y).length < m + 1
hy : 0 < 10 ^ (m + 1)
⊢ (Nat.digits 10 0).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
⊢ (Nat.digits 10 y).length < m + 1 + 1