Let x be given.
Assume Hx.
Apply xm (SNoR x = 0) to the current goal.
Assume H1: SNoR x = 0.
Apply orIL to the current goal.
An exact proof term for the current goal is H1.
Assume H1: SNoR x ≠ 0.
Apply orIR to the current goal.
We prove the intermediate claim L1: ∀y ∈ SNoR x, SNo y.
Let y be given.
Assume Hy.
Apply SNoS_E2 ω omega_ordinal x Hx to the current goal.
Assume _ _ Hx3 _.
Apply SNoR_E x Hx3 y Hy to the current goal.
Assume H _ _.
An exact proof term for the current goal is H.
An exact proof term for the current goal is finite_min_exists (SNoR x) L1 (SNoS_omega_SNoR_finite x Hx) H1.
∎