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