Let n be given.
Assume Hn.
Set L to be the term {0}.
Set R to be the term {eps_ m|m ∈ n}.
We prove the intermediate claim Ln: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim L1: SNoCutP L R.
An exact proof term for the current goal is eps_SNoCutP n Hn.
We prove the intermediate claim LRS: ∀z ∈ R, SNo z.
Apply L1 to the current goal.
Assume H _.
Apply H to the current goal.
Assume _ H.
An exact proof term for the current goal is H.
We prove the intermediate claim L2: (⋃x ∈ Lordsucc (SNoLev x)) = 1.
Apply set_ext to the current goal.
Let k be given.
Assume Hk.
Apply famunionE_impred L (λx ⇒ ordsucc (SNoLev x)) k Hk to the current goal.
Let w be given.
Assume Hw: w ∈ L.
rewrite the current goal using SingE 0 w Hw (from left to right).
rewrite the current goal using SNoLev_0 (from left to right).
Assume H2: k ∈ 1.
We will prove k ∈ 1.
An exact proof term for the current goal is H2.
Let i be given.
Assume Hi.
Apply cases_1 i Hi (λi ⇒ i ∈ ⋃x ∈ Lordsucc (SNoLev x)) to the current goal.
We will prove 0 ∈ ⋃x ∈ Lordsucc (SNoLev x).
Apply famunionI L (λx ⇒ ordsucc (SNoLev x)) 0 0 (SingI 0) to the current goal.
We will prove 0 ∈ ordsucc (SNoLev 0).
rewrite the current goal using SNoLev_0 (from left to right).
An exact proof term for the current goal is In_0_1.
We prove the intermediate claim L3: n ≠ 0 → (⋃y ∈ Rordsucc (SNoLev y)) = ordsucc n.
Assume Hn0: n ≠ 0.
Apply set_ext to the current goal.
Let k be given.
Assume Hk.
Apply famunionE_impred R (λy ⇒ ordsucc (SNoLev y)) k Hk to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Apply ReplE_impred n eps_ z Hz to the current goal.
Let m be given.
Assume Hm1: m ∈ n.
Assume Hm2: z = eps_ m.
rewrite the current goal using Hm2 (from left to right).
rewrite the current goal using SNoLev_eps_ m (nat_p_omega m (nat_p_trans n Ln m Hm1)) (from left to right).
Assume H2: k ∈ ordsucc (ordsucc m).
We will prove k ∈ ordsucc n.
We prove the intermediate claim L3a: ordsucc m ∈ ordsucc n.
Apply ordinal_ordsucc_In to the current goal.
We will prove ordinal n.
Apply nat_p_ordinal n to the current goal.
An exact proof term for the current goal is Ln.
An exact proof term for the current goal is Hm1.
We prove the intermediate claim L3b: ordsucc m ⊆ ordsucc n.
An exact proof term for the current goal is nat_trans (ordsucc n) (nat_ordsucc n Ln) (ordsucc m) L3a.
Apply ordsuccE (ordsucc m) k H2 to the current goal.
Assume H3: k ∈ ordsucc m.
Apply L3b to the current goal.
An exact proof term for the current goal is H3.
Assume H3: k = ordsucc m.
rewrite the current goal using H3 (from left to right).
An exact proof term for the current goal is L3a.
Let i be given.
Assume Hi: i ∈ ordsucc n.
We will prove i ∈ ⋃y ∈ Rordsucc (SNoLev y).
Apply nat_inv n Ln to the current goal.
Assume H2: n = 0.
We will prove False.
An exact proof term for the current goal is Hn0 H2.
Assume H2.
Apply H2 to the current goal.
Let n' be given.
Assume H2.
Apply H2 to the current goal.
Assume Hn'1: nat_p n'.
Assume Hn'2: n = ordsucc n'.
Apply famunionI R (λy ⇒ ordsucc (SNoLev y)) (eps_ n') i to the current goal.
We will prove eps_ n' ∈ R.
Apply ReplI to the current goal.
We will prove n' ∈ n.
rewrite the current goal using Hn'2 (from left to right).
Apply ordsuccI2 to the current goal.
We will prove i ∈ ordsucc (SNoLev (eps_ n')).
rewrite the current goal using SNoLev_eps_ n' (nat_p_omega n' Hn'1) (from left to right).
We will prove i ∈ ordsucc (ordsucc n').
rewrite the current goal using Hn'2 (from right to left).
An exact proof term for the current goal is Hi.
We prove the intermediate claim L4: (⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y)) = ordsucc n.
Apply xm (n = 0) to the current goal.
Assume H2: n = 0.
We prove the intermediate claim L4a: R = 0.
Apply Empty_eq to the current goal.
Let z be given.
Assume Hz.
Apply ReplE_impred n eps_ z Hz to the current goal.
Let m be given.
rewrite the current goal using H2 (from left to right).
Assume Hm1: m ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE m Hm1.
rewrite the current goal using L4a (from left to right).
rewrite the current goal using famunion_Empty (λy ⇒ ordsucc (SNoLev y)) (from left to right).
We will prove (⋃x ∈ Lordsucc (SNoLev x)) ∪ 0 = ordsucc n.
rewrite the current goal using binunion_idr (from left to right).
We will prove (⋃x ∈ Lordsucc (SNoLev x)) = ordsucc n.
rewrite the current goal using H2 (from left to right).
An exact proof term for the current goal is L2.
Assume H2: n ≠ 0.
rewrite the current goal using L3 H2 (from right to left).
rewrite the current goal using Subq_binunion_eq (from right to left).
rewrite the current goal using L2 (from left to right).
rewrite the current goal using L3 H2 (from left to right).
We will prove 1 ⊆ ordsucc n.
Let i be given.
Assume Hi.
Apply cases_1 i Hi (λi ⇒ i ∈ ordsucc n) to the current goal.
We will prove 0 ∈ ordsucc n.
Apply nat_0_in_ordsucc to the current goal.
An exact proof term for the current goal is Ln.
Apply SNoCutP_SNoCut_impred L R L1 to the current goal.
Assume H1: SNo (SNoCut L R).
rewrite the current goal using L4 (from left to right).
Assume H2: SNoLev (SNoCut L R) ∈ ordsucc (ordsucc n).
Assume H3: ∀w ∈ L, w < SNoCut L R.
Assume H4: ∀z ∈ R, SNoCut L R < z.
Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev (SNoCut L R) ⊆ SNoLev u ∧ SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) u.
We prove the intermediate claim L5: SNo (eps_ n).
An exact proof term for the current goal is SNo_eps_ n Hn.
We prove the intermediate claim L6: ∀w ∈ L, w < eps_ n.
Let w be given.
Assume Hw.
rewrite the current goal using SingE 0 w Hw (from left to right).
We will prove 0 < eps_ n.
An exact proof term for the current goal is SNo_eps_pos n Hn.
We prove the intermediate claim L7: ∀z ∈ R, eps_ n < z.
Let z be given.
Assume Hz.
Apply ReplE_impred n eps_ z Hz to the current goal.
Let m be given.
Assume Hm1: m ∈ n.
Assume Hm2: z = eps_ m.
rewrite the current goal using Hm2 (from left to right).
We will prove eps_ n < eps_ m.
An exact proof term for the current goal is SNo_eps_decr n Hn m Hm1.
Apply H5 (eps_ n) L5 L6 L7 to the current goal.
Assume H6: SNoLev (SNoCut L R) ⊆ SNoLev (eps_ n).
Assume H7: SNoEq_ (SNoLev (SNoCut L R)) (SNoCut L R) (eps_ n).
Use symmetry.
Apply SNo_eq (SNoCut L R) (eps_ n) H1 L5 to the current goal.
We will prove SNoLev (SNoCut L R) = SNoLev (eps_ n).
rewrite the current goal using SNoLev_eps_ n Hn (from left to right).
We will prove SNoLev (SNoCut L R) = ordsucc n.
Apply ordsuccE (ordsucc n) (SNoLev (SNoCut L R)) H2 to the current goal.
Assume H8: SNoLev (SNoCut L R) ∈ ordsucc n.
We will prove False.
We prove the intermediate claim L8: eps_ n < SNoCut L R.
Apply SNo_pos_eps_Lt n (omega_nat_p n Hn) (SNoCut L R) to the current goal.
We will prove SNoCut L R ∈ SNoS_ (ordsucc n).
Apply SNoS_I (ordsucc n) (nat_p_ordinal (ordsucc n) (nat_ordsucc n (omega_nat_p n Hn))) (SNoCut L R) (SNoLev (SNoCut L R)) H8 to the current goal.
We will prove SNo_ (SNoLev (SNoCut L R)) (SNoCut L R).
An exact proof term for the current goal is SNoLev_ (SNoCut L R) H1.
We will prove 0 < SNoCut L R.
Apply H3 to the current goal.
Apply SingI to the current goal.
Apply SNoLtE (eps_ n) (SNoCut L R) (SNo_eps_ n Hn) H1 L8 to the current goal.
Let z be given.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ SNoLev (eps_ n) ∩ SNoLev (SNoCut L R).
Assume Hz3: SNoEq_ (SNoLev z) z (eps_ n).
Assume Hz4: SNoEq_ (SNoLev z) z (SNoCut L R).
Assume Hz5: eps_ n < z.
Assume Hz6: z < SNoCut L R.
Assume Hz7: SNoLev z ∉ eps_ n.
Assume Hz8: SNoLev z ∈ SNoCut L R.
We prove the intermediate claim L9: ∀w ∈ L, w < z.
Let w be given.
Assume Hw.
rewrite the current goal using SingE 0 w Hw (from left to right).
We will prove 0 < z.
Apply SNoLt_tra 0 (eps_ n) z SNo_0 (SNo_eps_ n Hn) Hz1 to the current goal.
An exact proof term for the current goal is SNo_eps_pos n Hn.
An exact proof term for the current goal is Hz5.
We prove the intermediate claim L10: ∀v ∈ R, z < v.
Let v be given.
Assume Hv.
Apply SNoLt_tra z (SNoCut L R) v Hz1 H1 (LRS v Hv) Hz6 to the current goal.
We will prove SNoCut L R < v.
Apply H4 to the current goal.
An exact proof term for the current goal is Hv.
Apply H5 z Hz1 L9 L10 to the current goal.
Assume H9: SNoLev (SNoCut L R) ⊆ SNoLev z.
We will prove False.
Apply In_irref (SNoLev z) to the current goal.
Apply H9 to the current goal.
An exact proof term for the current goal is binintersectE2 (SNoLev (eps_ n)) (SNoLev (SNoCut L R)) (SNoLev z) Hz2.
rewrite the current goal using SNoLev_eps_ n Hn (from left to right).
Assume H9: ordsucc n ∈ SNoLev (SNoCut L R).
We will prove False.
An exact proof term for the current goal is In_no2cycle (SNoLev (SNoCut L R)) (ordsucc n) H8 H9.
rewrite the current goal using SNoLev_eps_ n Hn (from left to right).
Assume H9: SNoLev (SNoCut L R) ∈ ordsucc n.
Assume H10: SNoEq_ (SNoLev (SNoCut L R)) (eps_ n) (SNoCut L R).
Assume H11: SNoLev (SNoCut L R) ∉ eps_ n.
We prove the intermediate claim L11: ∃m ∈ n, SNoCut L R = eps_ m.
Apply eps_SNo_eq n (omega_nat_p n Hn) (SNoCut L R) to the current goal.
We will prove SNoCut L R ∈ SNoS_ (ordsucc n).
Apply SNoS_I (ordsucc n) (nat_p_ordinal (ordsucc n) (nat_ordsucc n (omega_nat_p n Hn))) (SNoCut L R) (SNoLev (SNoCut L R)) to the current goal.
We will prove SNoLev (SNoCut L R) ∈ ordsucc n.
An exact proof term for the current goal is H9.
We will prove SNo_ (SNoLev (SNoCut L R)) (SNoCut L R).
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is H1.
We will prove 0 < SNoCut L R.
Apply H3 to the current goal.
Apply SingI to the current goal.
We will prove SNoEq_ (SNoLev (SNoCut L R)) (eps_ n) (SNoCut L R).
An exact proof term for the current goal is H10.
Apply L11 to the current goal.
Let m be given.
Assume H12.
Apply H12 to the current goal.
Assume Hm1: m ∈ n.
Assume Hm2: SNoCut L R = eps_ m.
Apply SNoLt_irref (eps_ m) to the current goal.
We will prove eps_ m < eps_ m.
rewrite the current goal using Hm2 (from right to left) at position 1.
We will prove SNoCut L R < eps_ m.
Apply H4 to the current goal.
We will prove eps_ m ∈ {eps_ m|m ∈ n}.
Apply ReplI to the current goal.
An exact proof term for the current goal is Hm1.
Assume H8: SNoLev (SNoCut L R) = ordsucc n.
An exact proof term for the current goal is H8.
An exact proof term for the current goal is H7.
∎