induction k using induction_iSigmaZero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A k : M
⊢ k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n
case hP
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
⊢ 𝚺₀-Predicate fun {k} => k ≤ ‖A‖ → ∃ n ≤ k, NuonAux A k n

case zero
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A : M
⊢ 0 ≤ ‖A‖ → ∃ n ≤ 0, NuonAux A 0 n

case succ
M : Type u_1
inst✝⁵ : Zero M
inst✝⁴ : One M
inst✝³ : Add M
inst✝² : Mul M
inst✝¹ : LT M
inst✝ : M ⊧ₘ* 𝐈𝚫₀ + 𝛀₁
A x✝ : M
a✝ : x✝ ≤ ‖A‖ → ∃ n ≤ x✝, NuonAux A x✝ n
⊢ x✝ + 1 ≤ ‖A‖ → ∃ n ≤ x✝ + 1, NuonAux A (x✝ + 1) n