case succ k IH =>
  intro hk
  rcases IH (le_trans (by simp) hk) with ⟨n, hn, Hn⟩
  exact ⟨n + fbit A k, add_le_add hn (by simp), Hn.succ (le_trans (by simp) hk)⟩
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
IH : k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
⊢ k + 1 ≤ ‖A‖ → ∃ n ≤ k + 1, NuonAux A (k + 1) n
no goals