rcases NuonAux.exists hk with ⟨n', H'⟩
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
hk : k ≤ ‖A‖
H : NuonAux A (k + 1) n
⊢ ∃ n', n = n' + fbit A k ∧ NuonAux A k n'
case intro
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
n A k : M
hk : k ≤ ‖A‖
H : NuonAux A (k + 1) n
n' : M
H' : NuonAux A k n'
⊢ ∃ n', n = n' + fbit A k ∧ NuonAux A k n'