Let L be given.
Assume HL.
Let R be given.
Assume HR.
Assume HLR.
Apply HLR to the current goal.
Assume H.
Apply H to the current goal.
Assume HLR1: ∀w ∈ L, SNo w.
Assume HLR2: ∀z ∈ R, SNo z.
Assume HLR3: ∀w ∈ L, ∀z ∈ R, w < z.
Assume HL0: L ≠ 0.
Assume HR0: R ≠ 0.
Assume HL1: ∀w ∈ L, ∃w' ∈ L, w < w'.
Assume HR1: ∀z ∈ R, ∃z' ∈ R, z' < z.
Set x to be the term SNoCut L R.
Apply SNoCutP_SNoCut_impred L R HLR to the current goal.
Assume H1: SNo x.
Assume H2: SNoLev x ∈ ordsucc ((⋃x ∈ Lordsucc (SNoLev x)) ∪ (⋃y ∈ Rordsucc (SNoLev y))).
Assume H3: ∀w ∈ L, w < x.
Assume H4: ∀z ∈ R, x < z.
Assume H5: ∀u, SNo u → (∀w ∈ L, w < u) → (∀z ∈ R, u < z) → SNoLev x ⊆ SNoLev u ∧ SNoEq_ (SNoLev x) x u.
Set L_ to be the term λn ⇒ {w' ∈ SNoS_ n|∃w ∈ L, w' ≤ w} of type set → set.
Set R_ to be the term λn ⇒ {z' ∈ SNoS_ n|∃z ∈ R, z ≤ z'} of type set → set.
Set L' to be the term ⋃n ∈ ωL_ n.
Set R' to be the term ⋃n ∈ ωR_ n.
Set x' to be the term SNoCut L' R'.
We prove the intermediate claim LL'L: ∀w' ∈ L', ∃w ∈ L, w' ≤ w.
Let w' be given.
Assume Hw'.
Apply famunionE_impred ω L_ w' Hw' to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hw'2: w' ∈ L_ n.
An exact proof term for the current goal is SepE2 (SNoS_ n) (λw' ⇒ ∃w ∈ L, w' ≤ w) w' Hw'2.
We prove the intermediate claim LR'R: ∀z' ∈ R', ∃z ∈ R, z ≤ z'.
Let z' be given.
Assume Hz'.
Apply famunionE_impred ω R_ z' Hz' to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hz'2: z' ∈ R_ n.
An exact proof term for the current goal is SepE2 (SNoS_ n) (λz' ⇒ ∃z ∈ R, z ≤ z') z' Hz'2.
We prove the intermediate claim LL'o: L' ⊆ SNoS_ ω.
Let w' be given.
Assume Hw'.
Apply famunionE_impred ω L_ w' Hw' to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hw'2: w' ∈ L_ n.
Apply SNoS_E2 n (nat_p_ordinal n (omega_nat_p n Hn)) w' (SepE1 (SNoS_ n) (λw' ⇒ ∃w ∈ L, w' ≤ w) w' Hw'2) to the current goal.
Assume Hw'3: SNoLev w' ∈ n.
Assume Hw'4: ordinal (SNoLev w').
Assume Hw'5: SNo w'.
Assume Hw'6: SNo_ (SNoLev w') w'.
Apply SNoS_I ω omega_ordinal w' (SNoLev w') to the current goal.
We will prove SNoLev w' ∈ ω.
An exact proof term for the current goal is omega_TransSet n Hn (SNoLev w') Hw'3.
An exact proof term for the current goal is Hw'6.
We prove the intermediate claim LR'o: R' ⊆ SNoS_ ω.
Let z' be given.
Assume Hz'.
Apply famunionE_impred ω R_ z' Hz' to the current goal.
Let n be given.
Assume Hn: n ∈ ω.
Assume Hz'2: z' ∈ R_ n.
Apply SNoS_E2 n (nat_p_ordinal n (omega_nat_p n Hn)) z' (SepE1 (SNoS_ n) (λz' ⇒ ∃z ∈ R, z ≤ z') z' Hz'2) to the current goal.
Assume Hz'3: SNoLev z' ∈ n.
Assume Hz'4: ordinal (SNoLev z').
Assume Hz'5: SNo z'.
Assume Hz'6: SNo_ (SNoLev z') z'.
Apply SNoS_I ω omega_ordinal z' (SNoLev z') to the current goal.
We will prove SNoLev z' ∈ ω.
An exact proof term for the current goal is omega_TransSet n Hn (SNoLev z') Hz'3.
An exact proof term for the current goal is Hz'6.
We prove the intermediate claim LL': ∀w' ∈ L', SNo w'.
Let w' be given.
Assume Hw'.
Apply SNoS_E2 ω omega_ordinal w' (LL'o w' Hw') to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim LR': ∀z ∈ R', SNo z.
Let z' be given.
Assume Hz'.
Apply SNoS_E2 ω omega_ordinal z' (LR'o z' Hz') to the current goal.
Assume _ _ H _.
An exact proof term for the current goal is H.
We prove the intermediate claim LLR': SNoCutP L' R'.
We will prove (∀w ∈ L', SNo w) ∧ (∀z ∈ R', SNo z) ∧ (∀w ∈ L', ∀z ∈ R', w < z).
Apply and3I to the current goal.
An exact proof term for the current goal is LL'.
An exact proof term for the current goal is LR'.
Let w' be given.
Assume Hw'.
Let z' be given.
Assume Hz'.
Apply LL'L w' Hw' to the current goal.
Let w be given.
Assume H.
Apply H to the current goal.
Assume Hw: w ∈ L.
Assume Hw'w: w' ≤ w.
Apply LR'R z' Hz' to the current goal.
Let z be given.
Assume H.
Apply H to the current goal.
Assume Hz: z ∈ R.
Assume Hzz': z ≤ z'.
We will prove w' < z'.
Apply SNoLeLt_tra w' w z' (LL' w' Hw') (HLR1 w Hw) (LR' z' Hz') Hw'w to the current goal.
We will prove w < z'.
Apply SNoLtLe_tra w z z' (HLR1 w Hw) (HLR2 z Hz) (LR' z' Hz') to the current goal.
We will prove w < z.
Apply HLR3 to the current goal.
An exact proof term for the current goal is Hw.
An exact proof term for the current goal is Hz.
We will prove z ≤ z'.
An exact proof term for the current goal is Hzz'.
Apply SNoCutP_SNoCut_impred L' R' LLR' to the current goal.
Assume H1': SNo x'.
Assume H2': SNoLev x' ∈ ordsucc ((⋃x ∈ L'ordsucc (SNoLev x)) ∪ (⋃y ∈ R'ordsucc (SNoLev y))).
Assume H3': ∀w ∈ L', w < x'.
Assume H4': ∀z ∈ R', x' < z.
Assume H5': ∀u, SNo u → (∀w ∈ L', w < u) → (∀z ∈ R', u < z) → SNoLev x' ⊆ SNoLev u ∧ SNoEq_ (SNoLev x') x' u.
We prove the intermediate claim L1: ∀w ∈ L, ∃w' ∈ L', w ≤ w'.
Let w be given.
Assume Hw.
Apply real_E w (HL w Hw) to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ ordsucc ω.
Assume _ _ _ _ _.
Apply ordsuccE ω (SNoLev w) Hw2 to the current goal.
Assume H6: SNoLev w ∈ ω.
We use w to witness the existential quantifier.
Apply andI to the current goal.
We will prove w ∈ L'.
We will prove w ∈ famunion ω L_.
Apply famunionI ω L_ (ordsucc (SNoLev w)) w to the current goal.
We will prove ordsucc (SNoLev w) ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is H6.
We will prove w ∈ {w' ∈ SNoS_ (ordsucc (SNoLev w))|∃w ∈ L, w' ≤ w}.
Apply SepI to the current goal.
Apply SNoS_SNoLev to the current goal.
An exact proof term for the current goal is Hw1.
We will prove ∃u ∈ L, w ≤ u.
We use w to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw.
Apply SNoLe_ref to the current goal.
Apply SNoLe_ref to the current goal.
Assume H6: SNoLev w = ω.
Apply HL1 w Hw to the current goal.
Let w' be given.
Assume H.
Apply H to the current goal.
Assume Hw': w' ∈ L.
Assume Hww': w < w'.
Apply real_E w' (HL w' Hw') to the current goal.
Assume Hw'1: SNo w'.
Assume Hw'2: SNoLev w' ∈ ordsucc ω.
Assume _ _ _ _ _.
Apply ordsuccE ω (SNoLev w') Hw'2 to the current goal.
Assume H7: SNoLev w' ∈ ω.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
We will prove w' ∈ L'.
We will prove w' ∈ famunion ω L_.
Apply famunionI ω L_ (ordsucc (SNoLev w')) w' to the current goal.
We will prove ordsucc (SNoLev w') ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is H7.
We will prove w' ∈ {w' ∈ SNoS_ (ordsucc (SNoLev w'))|∃w ∈ L, w' ≤ w}.
Apply SepI to the current goal.
Apply SNoS_SNoLev to the current goal.
An exact proof term for the current goal is Hw'1.
We will prove ∃u ∈ L, w' ≤ u.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
Apply SNoLe_ref to the current goal.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hww'.
Assume H7: SNoLev w' = ω.
Apply SNoLtE w w' Hw1 Hw'1 Hww' to the current goal.
Let w'' be given.
rewrite the current goal using H6 (from left to right).
Assume Hw''1: SNo w''.
Assume Hw''2: SNoLev w'' ∈ ω ∩ SNoLev w'.
Assume _ _.
Assume Hw''3: w < w''.
Assume Hw''4: w'' < w'.
Assume _ _.
We use w'' to witness the existential quantifier.
Apply andI to the current goal.
We will prove w'' ∈ L'.
We will prove w'' ∈ famunion ω L_.
Apply famunionI ω L_ (ordsucc (SNoLev w'')) w'' to the current goal.
We will prove ordsucc (SNoLev w'') ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is binintersectE1 ω (SNoLev w') (SNoLev w'') Hw''2.
We will prove w'' ∈ {w' ∈ SNoS_ (ordsucc (SNoLev w''))|∃w ∈ L, w' ≤ w}.
Apply SepI to the current goal.
Apply SNoS_SNoLev to the current goal.
An exact proof term for the current goal is Hw''1.
We will prove ∃u ∈ L, w'' ≤ u.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hw''4.
We will prove w ≤ w''.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hw''3.
rewrite the current goal using H6 (from left to right).
rewrite the current goal using H7 (from left to right).
Assume H8: ω ∈ ω.
We will prove False.
An exact proof term for the current goal is In_irref ω H8.
rewrite the current goal using H6 (from left to right).
rewrite the current goal using H7 (from left to right).
Assume H8: ω ∈ ω.
We will prove False.
An exact proof term for the current goal is In_irref ω H8.
We prove the intermediate claim L2: ∀z ∈ R, ∃z' ∈ R', z' ≤ z.
Let z be given.
Assume Hz.
Apply real_E z (HR z Hz) to the current goal.
Assume Hz1: SNo z.
Assume Hz2: SNoLev z ∈ ordsucc ω.
Assume _ _ _ _ _.
Apply ordsuccE ω (SNoLev z) Hz2 to the current goal.
Assume H6: SNoLev z ∈ ω.
We use z to witness the existential quantifier.
Apply andI to the current goal.
We will prove z ∈ R'.
We will prove z ∈ famunion ω R_.
Apply famunionI ω R_ (ordsucc (SNoLev z)) z to the current goal.
We will prove ordsucc (SNoLev z) ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is H6.
We will prove z ∈ {z' ∈ SNoS_ (ordsucc (SNoLev z))|∃z ∈ R, z ≤ z'}.
Apply SepI to the current goal.
Apply SNoS_SNoLev to the current goal.
An exact proof term for the current goal is Hz1.
We will prove ∃u ∈ R, u ≤ z.
We use z to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz.
Apply SNoLe_ref to the current goal.
Apply SNoLe_ref to the current goal.
Assume H6: SNoLev z = ω.
Apply HR1 z Hz to the current goal.
Let z' be given.
Assume H.
Apply H to the current goal.
Assume Hz': z' ∈ R.
Assume Hz'z: z' < z.
Apply real_E z' (HR z' Hz') to the current goal.
Assume Hz'1: SNo z'.
Assume Hz'2: SNoLev z' ∈ ordsucc ω.
Assume _ _ _ _ _.
Apply ordsuccE ω (SNoLev z') Hz'2 to the current goal.
Assume H7: SNoLev z' ∈ ω.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
We will prove z' ∈ R'.
We will prove z' ∈ famunion ω R_.
Apply famunionI ω R_ (ordsucc (SNoLev z')) z' to the current goal.
We will prove ordsucc (SNoLev z') ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is H7.
We will prove z' ∈ {z' ∈ SNoS_ (ordsucc (SNoLev z'))|∃z ∈ R, z ≤ z'}.
Apply SepI to the current goal.
Apply SNoS_SNoLev to the current goal.
An exact proof term for the current goal is Hz'1.
We will prove ∃u ∈ R, u ≤ z'.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
Apply SNoLe_ref to the current goal.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz'z.
Assume H7: SNoLev z' = ω.
Apply SNoLtE z' z Hz'1 Hz1 Hz'z to the current goal.
Let z'' be given.
rewrite the current goal using H7 (from left to right).
Assume Hz''1: SNo z''.
Assume Hz''2: SNoLev z'' ∈ ω ∩ SNoLev z.
Assume _ _.
Assume Hz''3: z' < z''.
Assume Hz''4: z'' < z.
Assume _ _.
We use z'' to witness the existential quantifier.
Apply andI to the current goal.
We will prove z'' ∈ R'.
We will prove z'' ∈ famunion ω R_.
Apply famunionI ω R_ (ordsucc (SNoLev z'')) z'' to the current goal.
We will prove ordsucc (SNoLev z'') ∈ ω.
Apply omega_ordsucc to the current goal.
An exact proof term for the current goal is binintersectE1 ω (SNoLev z) (SNoLev z'') Hz''2.
We will prove z'' ∈ {z' ∈ SNoS_ (ordsucc (SNoLev z''))|∃z ∈ R, z ≤ z'}.
Apply SepI to the current goal.
Apply SNoS_SNoLev to the current goal.
An exact proof term for the current goal is Hz''1.
We will prove ∃u ∈ R, u ≤ z''.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz''3.
We will prove z'' ≤ z.
Apply SNoLtLe to the current goal.
An exact proof term for the current goal is Hz''4.
rewrite the current goal using H6 (from left to right).
rewrite the current goal using H7 (from left to right).
Assume H8: ω ∈ ω.
We will prove False.
An exact proof term for the current goal is In_irref ω H8.
rewrite the current goal using H6 (from left to right).
rewrite the current goal using H7 (from left to right).
Assume H8: ω ∈ ω.
We will prove False.
An exact proof term for the current goal is In_irref ω H8.
We prove the intermediate claim L3: L' ≠ 0.
Assume H6: L' = 0.
Apply HL0 to the current goal.
We will prove L = 0.
Apply Empty_eq to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Apply L1 w Hw to the current goal.
Let w' be given.
Assume H.
Apply H to the current goal.
Assume Hw': w' ∈ L'.
We will prove False.
Apply EmptyE w' to the current goal.
We will prove w' ∈ 0.
rewrite the current goal using H6 (from right to left).
An exact proof term for the current goal is Hw'.
We prove the intermediate claim L4: R' ≠ 0.
Assume H6: R' = 0.
Apply HR0 to the current goal.
We will prove R = 0.
Apply Empty_eq to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Apply L2 z Hz to the current goal.
Let z' be given.
Assume H.
Apply H to the current goal.
Assume Hz': z' ∈ R'.
We will prove False.
Apply EmptyE z' to the current goal.
We will prove z' ∈ 0.
rewrite the current goal using H6 (from right to left).
An exact proof term for the current goal is Hz'.
We prove the intermediate claim L5: ∀w ∈ L', ∃w' ∈ L', w < w'.
Let w be given.
Assume Hw.
Apply LL'L w Hw to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu: u ∈ L.
Assume Hwu: w ≤ u.
Apply HL1 u Hu to the current goal.
Let v be given.
Assume H.
Apply H to the current goal.
Assume Hv: v ∈ L.
Assume Huv: u < v.
Apply L1 v Hv to the current goal.
Let w' be given.
Assume H.
Apply H to the current goal.
Assume Hw': w' ∈ L'.
Assume Hvw': v ≤ w'.
We use w' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hw'.
We will prove w < w'.
Apply SNoLeLt_tra w u w' (LL' w Hw) (HLR1 u Hu) (LL' w' Hw') Hwu to the current goal.
We will prove u < w'.
An exact proof term for the current goal is SNoLtLe_tra u v w' (HLR1 u Hu) (HLR1 v Hv) (LL' w' Hw') Huv Hvw'.
We prove the intermediate claim L6: ∀z ∈ R', ∃z' ∈ R', z' < z.
Let z be given.
Assume Hz.
Apply LR'R z Hz to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu: u ∈ R.
Assume Huz: u ≤ z.
Apply HR1 u Hu to the current goal.
Let v be given.
Assume H.
Apply H to the current goal.
Assume Hv: v ∈ R.
Assume Hvu: v < u.
Apply L2 v Hv to the current goal.
Let z' be given.
Assume H.
Apply H to the current goal.
Assume Hz': z' ∈ R'.
Assume Hz'v: z' ≤ v.
We use z' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hz'.
We will prove z' < z.
Apply SNoLeLt_tra z' v z (LR' z' Hz') (HLR2 v Hv) (LR' z Hz) Hz'v to the current goal.
We will prove v < z.
An exact proof term for the current goal is SNoLtLe_tra v u z (HLR2 v Hv) (HLR2 u Hu) (LR' z Hz) Hvu Huz.
We prove the intermediate claim Lxx': x = x'.
Apply SNoCut_ext to the current goal.
An exact proof term for the current goal is HLR.
An exact proof term for the current goal is LLR'.
Let w be given.
Assume Hw: w ∈ L.
We will prove w < x'.
Apply L1 w Hw to the current goal.
Let w' be given.
Assume H.
Apply H to the current goal.
Assume Hw': w' ∈ L'.
Assume Hww': w ≤ w'.
Apply SNoLeLt_tra w w' x' to the current goal.
We will prove SNo w.
An exact proof term for the current goal is HLR1 w Hw.
We will prove SNo w'.
An exact proof term for the current goal is LL' w' Hw'.
We will prove SNo x'.
An exact proof term for the current goal is H1'.
An exact proof term for the current goal is Hww'.
We will prove w' < x'.
Apply H3' to the current goal.
We will prove w' ∈ L'.
An exact proof term for the current goal is Hw'.
Let z be given.
Assume Hz: z ∈ R.
We will prove x' < z.
Apply L2 z Hz to the current goal.
Let z' be given.
Assume H.
Apply H to the current goal.
Assume Hz': z' ∈ R'.
Assume Hz'z: z' ≤ z.
We will prove x' < z.
An exact proof term for the current goal is SNoLtLe_tra x' z' z H1' (LR' z' Hz') (HLR2 z Hz) (H4' z' Hz') Hz'z.
Let w be given.
Assume Hw: w ∈ L'.
We will prove w < x.
Apply LL'L w Hw to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu: u ∈ L.
Assume Hwu: w ≤ u.
An exact proof term for the current goal is SNoLeLt_tra w u x (LL' w Hw) (HLR1 u Hu) H1 Hwu (H3 u Hu).
Let z be given.
Assume Hz: z ∈ R'.
We will prove x < z.
Apply LR'R z Hz to the current goal.
Let u be given.
Assume H.
Apply H to the current goal.
Assume Hu: u ∈ R.
Assume Huz: u ≤ z.
An exact proof term for the current goal is SNoLtLe_tra x u z H1 (HLR2 u Hu) (LR' z Hz) (H4 u Hu) Huz.
We will prove x ∈ real.
rewrite the current goal using Lxx' (from left to right).
We will prove x' ∈ real.
An exact proof term for the current goal is real_SNoCut_SNoS_omega L' LL'o R' LR'o LLR' L3 L4 L5 L6.
∎