Let n be given.
Assume Hn: nat_p n.
Let x be given.
Assume Hx: x ∈ SNoS_ (ordsucc n).
Assume Hxpos: 0 < x.
We prove the intermediate claim Ln: n ∈ ω.
An exact proof term for the current goal is nat_p_omega n Hn.
Apply SNoS_E2 (ordsucc n) (nat_p_ordinal (ordsucc n) (nat_ordsucc n Hn)) x Hx to the current goal.
Assume Hx1: SNoLev x ∈ ordsucc n.
Assume Hx2: ordinal (SNoLev x).
Assume Hx3: SNo x.
Assume Hx4: SNo_ (SNoLev x) x.
We will prove eps_ n < x.
Apply SNoLt_trichotomy_or_impred (eps_ n) x (SNo_eps_ n Ln) Hx3 to the current goal.
Assume H2: eps_ n < x.
An exact proof term for the current goal is H2.
Assume H2: eps_ n = x.
We will prove False.
Apply In_irref (ordsucc n) to the current goal.
rewrite the current goal using SNoLev_eps_ n Ln (from right to left) at position 1.
We will prove SNoLev (eps_ n) ∈ ordsucc n.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is Hx1.
Assume H2: x < eps_ n.
We will prove False.
Apply SNoLtE x (eps_ n) Hx3 (SNo_eps_ n Ln) H2 to the current goal.
Let z be given.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev x ∩ SNoLev (eps_ n).
Assume Hz3: SNoEq_ (SNoLev z) z x.
Assume Hz4: SNoEq_ (SNoLev z) z (eps_ n).
Assume Hz5: x < z.
Assume Hz6: z < eps_ n.
Assume Hz7: SNoLev z ∉ x.
Assume Hz8: SNoLev z ∈ eps_ n.
We prove the intermediate claim Lz0: z = 0.
Apply SNoLev_0_eq_0 z Hz1 to the current goal.
An exact proof term for the current goal is eps_ordinal_In_eq_0 n (SNoLev z) (SNoLev_ordinal z Hz1) Hz8.
Apply SNoLt_irref x to the current goal.
We will prove x < x.
Apply SNoLt_tra x z x Hx3 Hz1 Hx3 Hz5 to the current goal.
We will prove z < x.
rewrite the current goal using Lz0 (from left to right).
An exact proof term for the current goal is Hxpos.
Assume H1: SNoLev x ∈ SNoLev (eps_ n).
Assume H2: SNoEq_ (SNoLev x) x (eps_ n).
Assume H3: SNoLev x ∈ (eps_ n).
We prove the intermediate claim Lx0: x = 0.
Apply SNoLev_0_eq_0 x Hx3 to the current goal.
An exact proof term for the current goal is eps_ordinal_In_eq_0 n (SNoLev x) Hx2 H3.
Apply SNoLt_irref x to the current goal.
rewrite the current goal using Lx0 (from left to right) at position 1.
An exact proof term for the current goal is Hxpos.
rewrite the current goal using SNoLev_eps_ n Ln (from left to right).
Assume H1: ordsucc n ∈ SNoLev x.
We will prove False.
An exact proof term for the current goal is In_no2cycle (SNoLev x) (ordsucc n) Hx1 H1.
∎