Apply SNoLev_ind to the current goal.
Let x be given.
Assume Hx: SNo x.
Assume IH: ∀w ∈ SNoS_ (SNoLev x), SNo (- w) ∧ (∀u ∈ SNoL w, - w < - u) ∧ (∀u ∈ SNoR w, - u < - w) ∧ SNoCutP {- z|z ∈ SNoR w} {- v|v ∈ SNoL w}.
We prove the intermediate claim IHLx: ∀w ∈ SNoL x, SNo (- w) ∧ (∀u ∈ SNoL w, - w < - u) ∧ (∀u ∈ SNoR w, - u < - w).
Let w be given.
Assume Hw: w ∈ SNoL x.
Apply SNoL_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: w < x.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
Apply IH w Lw to the current goal.
Assume H _.
An exact proof term for the current goal is H.
We prove the intermediate claim IHRx: ∀z ∈ SNoR x, SNo (- z) ∧ (∀u ∈ SNoL z, - z < - u) ∧ (∀u ∈ SNoR z, - u < - z).
Let w be given.
Assume Hw: w ∈ SNoR x.
Apply SNoR_E x Hx w Hw to the current goal.
Assume Hw1: SNo w.
Assume Hw2: SNoLev w ∈ SNoLev x.
Assume Hw3: x < w.
We prove the intermediate claim Lw: w ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 w x Hw1 Hx Hw2.
Apply IH w Lw to the current goal.
Assume H _.
An exact proof term for the current goal is H.
Set L to be the term {- z|z ∈ SNoR x}.
Set R to be the term {- w|w ∈ SNoL x}.
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.
Let w be given.
Assume Hw: w ∈ L.
We will prove SNo w.
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw to the current goal.
Let z be given.
Assume Hz: z ∈ SNoR x.
Assume Hwz: w = - z.
Apply IHRx z Hz to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo (- z).
Assume _ _.
We will prove SNo w.
rewrite the current goal using Hwz (from left to right).
An exact proof term for the current goal is H2.
Let z be given.
Assume Hz: z ∈ R.
We will prove SNo z.
Apply ReplE_impred (SNoL x) (λw ⇒ - w) z Hz to the current goal.
Let w be given.
Assume Hw: w ∈ SNoL x.
Assume Hzw: z = - w.
Apply IHLx w Hw to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo (- w).
Assume _ _.
We will prove SNo z.
rewrite the current goal using Hzw (from left to right).
An exact proof term for the current goal is H2.
Let w be given.
Assume Hw: w ∈ L.
Let z be given.
Assume Hz: z ∈ R.
Apply ReplE_impred (SNoR x) (λz ⇒ - z) w Hw to the current goal.
Let u be given.
Assume Hu: u ∈ SNoR x.
Assume Hwu: w = - u.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
Apply SNoLev_prop u Hu1 to the current goal.
Assume Hu1a: ordinal (SNoLev u).
Assume Hu1b: SNo_ (SNoLev u) u.
Apply ReplE_impred (SNoL x) (λw ⇒ - w) z Hz to the current goal.
Let v be given.
Assume Hv: v ∈ SNoL x.
Assume Hzv: z = - v.
Apply SNoL_E x Hx v Hv to the current goal.
Assume Hv1: SNo v.
Assume Hv2: SNoLev v ∈ SNoLev x.
Assume Hv3: v < x.
Apply SNoLev_prop v Hv1 to the current goal.
Assume Hv1a: ordinal (SNoLev v).
Assume Hv1b: SNo_ (SNoLev v) v.
Apply IHLx v Hv to the current goal.
Assume H2.
Apply H2 to the current goal.
Assume H2: SNo (- v).
Assume H3: ∀u ∈ SNoL v, - v < - u.
Assume H4: ∀u ∈ SNoR v, - u < - v.
Apply IHRx u Hu to the current goal.
Assume H5.
Apply H5 to the current goal.
Assume H5: SNo (- u).
Assume H6: ∀v ∈ SNoL u, - u < - v.
Assume H7: ∀v ∈ SNoR u, - v < - u.
We will prove w < z.
rewrite the current goal using Hwu (from left to right).
rewrite the current goal using Hzv (from left to right).
We will prove - u < - v.
We prove the intermediate claim Lvu: v < u.
An exact proof term for the current goal is SNoLt_tra v x u Hv1 Hx Hu1 Hv3 Hu3.
Apply SNoLtE v u Hv1 Hu1 Lvu to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume Hz1: SNoLev z ∈ SNoLev v ∩ SNoLev u.
Assume Hz2: SNoEq_ (SNoLev z) z v.
Assume Hz3: SNoEq_ (SNoLev z) z u.
Assume Hz4: v < z.
Assume Hz5: z < u.
Assume Hz6: SNoLev z ∉ v.
Assume Hz7: SNoLev z ∈ u.
Apply SNoLev_prop z Hz to the current goal.
Assume Hza: ordinal (SNoLev z).
Assume Hzb: SNo_ (SNoLev z) z.
Apply binintersectE (SNoLev v) (SNoLev u) (SNoLev z) Hz1 to the current goal.
Assume Hz1a: SNoLev z ∈ SNoLev v.
Assume Hz1b: SNoLev z ∈ SNoLev u.
We prove the intermediate claim LzLx: z ∈ SNoS_ (SNoLev x).
Apply SNoS_I2 z x Hz Hx to the current goal.
We will prove SNoLev z ∈ SNoLev x.
Apply SNoLev_ordinal x Hx to the current goal.
Assume Hx2: TransSet (SNoLev x).
Assume _.
An exact proof term for the current goal is Hx2 (SNoLev u) Hu2 (SNoLev z) Hz1b.
We prove the intermediate claim Lmz: SNo (- z).
Apply IH z LzLx to the current goal.
Assume H.
Apply H 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 will prove - u < - v.
Apply SNoLt_tra (- u) (- z) (- v) H5 Lmz H2 to the current goal.
We will prove - u < - z.
Apply H6 to the current goal.
We will prove z ∈ SNoL u.
We will prove z ∈ {x ∈ SNoS_ (SNoLev u)|x < u}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev u).
Apply SNoS_I2 z u Hz Hu1 Hz1b to the current goal.
We will prove z < u.
An exact proof term for the current goal is Hz5.
We will prove - z < - v.
Apply H4 to the current goal.
We will prove z ∈ SNoR v.
We will prove z ∈ {x ∈ SNoS_ (SNoLev v)|v < x}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev v).
An exact proof term for the current goal is SNoS_I2 z v Hz Hv1 Hz1a.
We will prove v < z.
An exact proof term for the current goal is Hz4.
Assume H8: SNoLev v ∈ SNoLev u.
Assume H9: SNoEq_ (SNoLev v) v u.
Assume H10: SNoLev v ∈ u.
We will prove - u < - v.
Apply H6 to the current goal.
We will prove v ∈ SNoL u.
We will prove v ∈ {x ∈ SNoS_ (SNoLev u)|x < u}.
Apply SepI to the current goal.
We will prove v ∈ SNoS_ (SNoLev u).
An exact proof term for the current goal is SNoS_I2 v u Hv1 Hu1 H8.
We will prove v < u.
An exact proof term for the current goal is Lvu.
Assume H8: SNoLev u ∈ SNoLev v.
Assume H9: SNoEq_ (SNoLev u) v u.
Assume H10: SNoLev u ∉ v.
We will prove - u < - v.
Apply H4 to the current goal.
We will prove u ∈ SNoR v.
We will prove u ∈ {x ∈ SNoS_ (SNoLev v)|v < x}.
Apply SepI to the current goal.
We will prove u ∈ SNoS_ (SNoLev v).
An exact proof term for the current goal is SNoS_I2 u v Hu1 Hv1 H8.
We will prove v < u.
An exact proof term for the current goal is Lvu.
We prove the intermediate claim LNLR: SNo (SNoCut L R).
An exact proof term for the current goal is SNoCutP_SNo_SNoCut L R LLR.
Apply andI to the current goal.
rewrite the current goal using minus_SNo_eq x Hx (from left to right).
Apply and3I to the current goal.
We will prove SNo (SNoCut L R).
An exact proof term for the current goal is LNLR.
We will prove ∀u ∈ SNoL x, SNoCut L R < - u.
Let u be given.
Assume Hu: u ∈ SNoL x.
We will prove SNoCut L R < - u.
Apply SNoL_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: u < x.
We prove the intermediate claim LmuR: - u ∈ R.
Apply ReplI to the current goal.
We will prove u ∈ SNoL x.
An exact proof term for the current goal is Hu.
We will prove SNoCut L R < - u.
An exact proof term for the current goal is SNoCutP_SNoCut_R L R LLR (- u) LmuR.
We will prove ∀u ∈ SNoR x, - u < SNoCut L R.
Let u be given.
Assume Hu: u ∈ SNoR x.
We will prove - u < SNoCut L R.
Apply SNoR_E x Hx u Hu to the current goal.
Assume Hu1: SNo u.
Assume Hu2: SNoLev u ∈ SNoLev x.
Assume Hu3: x < u.
We prove the intermediate claim LmuL: - u ∈ L.
Apply ReplI to the current goal.
We will prove u ∈ SNoR x.
An exact proof term for the current goal is Hu.
We will prove - u < SNoCut L R.
An exact proof term for the current goal is SNoCutP_SNoCut_L L R LLR (- u) LmuL.
We will prove SNoCutP L R.
An exact proof term for the current goal is LLR.
∎