rcases H.uniq (H'.succ hk)
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'
case intro.refl
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
hk : k ≤ ‖A‖
n' : M
H' : NuonAux A k n'
H : NuonAux A (k + 1) (n' + fbit A k)
⊢ ∃ n'_1, n' + fbit A k = n'_1 + fbit A k ∧ NuonAux A k n'_1