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.
We prove the intermediate claim Lo: ordinal ((⋃w ∈ Lordsucc (SNoLev w)) ∪ (⋃z ∈ Rordsucc (SNoLev z))).
Apply ordinal_binunion to the current goal.
Apply ordinal_famunion to the current goal.
Let w be given.
Assume Hw.
We will prove ordinal (ordsucc (SNoLev w)).
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev w).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is HLR1 w Hw.
Apply ordinal_famunion to the current goal.
Let z be given.
Assume Hz.
We will prove ordinal (ordsucc (SNoLev z)).
Apply ordinal_ordsucc to the current goal.
We will prove ordinal (SNoLev z).
Apply SNoLev_ordinal to the current goal.
An exact proof term for the current goal is HLR2 z Hz.
We prove the intermediate claim LLRsoo: ordsucc ((⋃w ∈ Lordsucc (SNoLev w)) ∪ (⋃z ∈ Rordsucc (SNoLev z))) ⊆ ordsucc ω.
Apply ordinal_ordsucc_In_Subq (ordsucc ω) ordsucc_omega_ordinal ((⋃w ∈ Lordsucc (SNoLev w)) ∪ (⋃z ∈ Rordsucc (SNoLev z))) to the current goal.
We will prove ((⋃w ∈ Lordsucc (SNoLev w)) ∪ (⋃z ∈ Rordsucc (SNoLev z))) ∈ ordsucc ω.
Apply ordinal_In_Or_Subq ((⋃w ∈ Lordsucc (SNoLev w)) ∪ (⋃z ∈ Rordsucc (SNoLev z))) (ordsucc ω) Lo ordsucc_omega_ordinal to the current goal.
Assume H6.
An exact proof term for the current goal is H6.
Assume H6: ordsucc ω ⊆ (⋃w ∈ Lordsucc (SNoLev w)) ∪ (⋃z ∈ Rordsucc (SNoLev z)).
We will prove False.
Apply binunionE (⋃w ∈ Lordsucc (SNoLev w)) (⋃z ∈ Rordsucc (SNoLev z)) ω (H6 ω (ordsuccI2 ω)) to the current goal.
Assume H7: ω ∈ ⋃w ∈ Lordsucc (SNoLev w).
Apply famunionE_impred L (λw ⇒ ordsucc (SNoLev w)) ω H7 to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Assume H8: ω ∈ ordsucc (SNoLev w).
Apply SNoS_E2 ω omega_ordinal w (HL w Hw) to the current goal.
Assume Hw1: SNoLev w ∈ ω.
We will prove False.
Apply ordsuccE (SNoLev w) ω H8 to the current goal.
Assume H9: ω ∈ SNoLev w.
An exact proof term for the current goal is In_no2cycle ω (SNoLev w) H9 Hw1.
Assume H9: ω = SNoLev w.
We will prove False.
Apply In_irref ω to the current goal.
rewrite the current goal using H9 (from left to right) at position 1.
An exact proof term for the current goal is Hw1.
Assume H7: ω ∈ ⋃z ∈ Rordsucc (SNoLev z).
Apply famunionE_impred R (λz ⇒ ordsucc (SNoLev z)) ω H7 to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Assume H8: ω ∈ ordsucc (SNoLev z).
Apply SNoS_E2 ω omega_ordinal z (HR z Hz) to the current goal.
Assume Hz1: SNoLev z ∈ ω.
We will prove False.
Apply ordsuccE (SNoLev z) ω H8 to the current goal.
Assume H9: ω ∈ SNoLev z.
An exact proof term for the current goal is In_no2cycle ω (SNoLev z) H9 Hz1.
Assume H9: ω = SNoLev z.
We will prove False.
Apply In_irref ω to the current goal.
rewrite the current goal using H9 (from left to right) at position 1.
An exact proof term for the current goal is Hz1.
Apply ordsuccE ω (SNoLev x) (LLRsoo (SNoLev x) H2) to the current goal.
Assume H6: SNoLev x ∈ ω.
We will prove x ∈ real.
Apply SNoS_omega_real to the current goal.
We will prove x ∈ SNoS_ ω.
Apply SNoS_I ω omega_ordinal x (SNoLev x) H6 to the current goal.
We will prove SNo_ (SNoLev x) x.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is H1.
Assume H6: SNoLev x = ω.
We will prove x ∈ real.
Apply real_I to the current goal.
We will prove x ∈ SNoS_ (ordsucc ω).
Apply SNoS_I (ordsucc ω) ordsucc_omega_ordinal x (SNoLev x) to the current goal.
We will prove SNoLev x ∈ ordsucc ω.
rewrite the current goal using H6 (from left to right).
Apply ordsuccI2 to the current goal.
We will prove SNo_ (SNoLev x) x.
Apply SNoLev_ to the current goal.
An exact proof term for the current goal is H1.
Assume H7: x = ω.
Apply HR0 to the current goal.
Apply Empty_eq to the current goal.
Let z be given.
Assume Hz: z ∈ R.
Apply SNoLt_irref z to the current goal.
We will prove z < z.
Apply SNoLt_tra z x z (HLR2 z Hz) H1 (HLR2 z Hz) to the current goal.
We will prove z < x.
rewrite the current goal using H7 (from left to right).
We will prove z < ω.
Apply ordinal_SNoLev_max ω omega_ordinal z (HLR2 z Hz) to the current goal.
We will prove SNoLev z ∈ ω.
Apply SNoS_E2 ω omega_ordinal z (HR z Hz) to the current goal.
Assume Hz1: SNoLev z ∈ ω.
Assume _ _ _.
An exact proof term for the current goal is Hz1.
We will prove x < z.
Apply H4 to the current goal.
An exact proof term for the current goal is Hz.
Assume H7: x = - ω.
Apply HL0 to the current goal.
Apply Empty_eq to the current goal.
Let w be given.
Assume Hw: w ∈ L.
Apply SNoLt_irref w to the current goal.
We will prove w < w.
Apply SNoLt_tra w x w (HLR1 w Hw) H1 (HLR1 w Hw) to the current goal.
We will prove w < x.
Apply H3 to the current goal.
An exact proof term for the current goal is Hw.
We will prove x < w.
rewrite the current goal using H7 (from left to right).
We will prove - ω < w.
Apply minus_SNo_Lt_contra1 w ω (HLR1 w Hw) SNo_omega to the current goal.
We will prove - w < ω.
Apply ordinal_SNoLev_max ω omega_ordinal (- w) (SNo_minus_SNo w (HLR1 w Hw)) to the current goal.
We will prove SNoLev (- w) ∈ ω.
rewrite the current goal using minus_SNo_Lev w (HLR1 w Hw) (from left to right).
Apply SNoS_E2 ω omega_ordinal w (HL w Hw) to the current goal.
Assume Hw1: SNoLev w ∈ ω.
Assume _ _ _.
An exact proof term for the current goal is Hw1.
Let q be given.
Assume Hq: q ∈ SNoS_ ω.
Assume H7: ∀k ∈ ω, abs_SNo (q + - x) < eps_ k.
We will prove False.
Apply SNoS_E2 ω omega_ordinal q Hq to the current goal.
Assume Hq1: SNoLev q ∈ ω.
Assume Hq2: ordinal (SNoLev q).
Assume Hq3: SNo q.
Assume Hq4: SNo_ (SNoLev q) q.
We prove the intermediate claim LqL: ∀w ∈ L, w < q.
Let w be given.
Assume Hw: w ∈ L.
Apply SNoLtLe_or w q (HLR1 w Hw) Hq3 to the current goal.
Assume H8: w < q.
An exact proof term for the current goal is H8.
Assume H8: q ≤ w.
We will prove False.
Apply HL1 w Hw to the current goal.
Let w' be given.
Assume H.
Apply H to the current goal.
Assume H9: w' ∈ L.
Assume H10: w < w'.
We prove the intermediate claim LqL1: w' + - q ∈ SNoS_ ω.
Apply add_SNo_SNoS_omega to the current goal.
An exact proof term for the current goal is HL w' H9.
Apply minus_SNo_SNoS_omega to the current goal.
An exact proof term for the current goal is Hq.
Apply SNoS_E2 ω omega_ordinal (w' + - q) LqL1 to the current goal.
Assume Hw'q1: SNoLev (w' + - q) ∈ ω.
Assume Hw'q2: ordinal (SNoLev (w' + - q)).
Assume Hw'q3: SNo (w' + - q).
Assume Hw'q4: SNo_ (SNoLev (w' + - q)) (w' + - q).
We prove the intermediate claim LqL2: 0 < w' + - q.
Apply SNoLt_minus_pos q w' Hq3 (HLR1 w' H9) to the current goal.
We will prove q < w'.
An exact proof term for the current goal is SNoLeLt_tra q w w' Hq3 (HLR1 w Hw) (HLR1 w' H9) H8 H10.
Set k to be the term SNoLev (w' + - q).
We prove the intermediate claim LqL3: w' + - q ∈ SNoS_ (ordsucc k).
An exact proof term for the current goal is SNoS_I (ordsucc k) (ordinal_ordsucc k (nat_p_ordinal k (omega_nat_p k Hw'q1))) (w' + - q) k (ordsuccI2 k) Hw'q4.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hw'q1.
We prove the intermediate claim LqL4: eps_ k < w' + - q.
An exact proof term for the current goal is SNo_pos_eps_Lt k (omega_nat_p k Hw'q1) (w' + - q) LqL3 LqL2.
Apply SNoLt_irref (eps_ k) to the current goal.
Apply SNoLt_tra (eps_ k) (w' + - q) (eps_ k) Lek Hw'q3 Lek LqL4 to the current goal.
We will prove w' + - q < eps_ k.
We prove the intermediate claim Lxq: SNo (x + - q).
An exact proof term for the current goal is SNo_add_SNo x (- q) H1 (SNo_minus_SNo q Hq3).
Apply SNoLt_tra (w' + - q) (x + - q) (eps_ k) Hw'q3 Lxq Lek to the current goal.
We will prove w' + - q < x + - q.
Apply add_SNo_Lt1 w' (- q) x (HLR1 w' H9) (SNo_minus_SNo q Hq3) H1 to the current goal.
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 H9.
We will prove x + - q < eps_ k.
Apply SNoLtLe_or (x + - q) 0 Lxq SNo_0 to the current goal.
Assume H11: x + - q < 0.
An exact proof term for the current goal is SNoLt_tra (x + - q) 0 (eps_ k) Lxq SNo_0 Lek H11 (SNo_eps_pos k Hw'q1).
Assume H11: 0 ≤ x + - q.
rewrite the current goal using nonneg_abs_SNo (x + - q) H11 (from right to left).
We will prove abs_SNo (x + - q) < eps_ k.
rewrite the current goal using abs_SNo_dist_swap x q H1 Hq3 (from left to right).
An exact proof term for the current goal is H7 k Hw'q1.
We prove the intermediate claim LqR: ∀z ∈ R, q < z.
Let z be given.
Assume Hz: z ∈ R.
Apply SNoLtLe_or q z Hq3 (HLR2 z Hz) to the current goal.
Assume H8: q < z.
An exact proof term for the current goal is H8.
Assume H8: z ≤ q.
We will prove False.
Apply HR1 z Hz to the current goal.
Let z' be given.
Assume H.
Apply H to the current goal.
Assume H9: z' ∈ R.
Assume H10: z' < z.
We prove the intermediate claim LqR1: q + - z' ∈ SNoS_ ω.
Apply add_SNo_SNoS_omega to the current goal.
An exact proof term for the current goal is Hq.
Apply minus_SNo_SNoS_omega to the current goal.
An exact proof term for the current goal is HR z' H9.
Apply SNoS_E2 ω omega_ordinal (q + - z') LqR1 to the current goal.
Assume Hz'q1: SNoLev (q + - z') ∈ ω.
Assume Hz'q2: ordinal (SNoLev (q + - z')).
Assume Hz'q3: SNo (q + - z').
Assume Hz'q4: SNo_ (SNoLev (q + - z')) (q + - z').
We prove the intermediate claim LqR2: 0 < q + - z'.
Apply SNoLt_minus_pos z' q (HLR2 z' H9) Hq3 to the current goal.
We will prove z' < q.
An exact proof term for the current goal is SNoLtLe_tra z' z q (HLR2 z' H9) (HLR2 z Hz) Hq3 H10 H8.
Set k to be the term SNoLev (q + - z').
We prove the intermediate claim LqR3: q + - z' ∈ SNoS_ (ordsucc k).
An exact proof term for the current goal is SNoS_I (ordsucc k) (ordinal_ordsucc k (nat_p_ordinal k (omega_nat_p k Hz'q1))) (q + - z') k (ordsuccI2 k) Hz'q4.
We prove the intermediate claim Lek: SNo (eps_ k).
An exact proof term for the current goal is SNo_eps_ k Hz'q1.
We prove the intermediate claim LqR4: eps_ k < q + - z'.
An exact proof term for the current goal is SNo_pos_eps_Lt k (omega_nat_p k Hz'q1) (q + - z') LqR3 LqR2.
Apply SNoLt_irref (eps_ k) to the current goal.
Apply SNoLt_tra (eps_ k) (q + - z') (eps_ k) Lek Hz'q3 Lek LqR4 to the current goal.
We will prove q + - z' < eps_ k.
We prove the intermediate claim Lxq: SNo (q + - x).
An exact proof term for the current goal is SNo_add_SNo q (- x) Hq3 (SNo_minus_SNo x H1).
Apply SNoLt_tra (q + - z') (q + - x) (eps_ k) Hz'q3 Lxq Lek to the current goal.
We will prove q + - z' < q + - x.
Apply add_SNo_Lt2 q (- z') (- x) Hq3 (SNo_minus_SNo z' (HLR2 z' H9)) (SNo_minus_SNo x H1) to the current goal.
We will prove - z' < - x.
Apply minus_SNo_Lt_contra x z' H1 (HLR2 z' H9) to the current goal.
We will prove x < z'.
Apply H4 to the current goal.
We will prove z' ∈ R.
An exact proof term for the current goal is H9.
We will prove q + - x < eps_ k.
Apply SNoLtLe_or (q + - x) 0 Lxq SNo_0 to the current goal.
Assume H11: q + - x < 0.
An exact proof term for the current goal is SNoLt_tra (q + - x) 0 (eps_ k) Lxq SNo_0 Lek H11 (SNo_eps_pos k Hz'q1).
Assume H11: 0 ≤ q + - x.
rewrite the current goal using nonneg_abs_SNo (q + - x) H11 (from right to left).
We will prove abs_SNo (q + - x) < eps_ k.
An exact proof term for the current goal is H7 k Hz'q1.
Apply H5 q Hq3 LqL LqR to the current goal.
Assume H10: SNoLev x ⊆ SNoLev q.
We will prove False.
Apply In_irref (SNoLev q) to the current goal.
Apply H10 to the current goal.
We will prove SNoLev q ∈ SNoLev x.
rewrite the current goal using H6 (from left to right).
An exact proof term for the current goal is Hq1.
∎