Let x and y be given.
Assume Hx: SNo x.
Assume Hy: SNo y.
Assume Hxy: x < y.
Apply minus_SNo_prop1 x Hx to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1.
Apply H1 to the current goal.
Assume H1: SNo (- x).
Assume H2: ∀u ∈ SNoL x, - x < - u.
Assume H3: ∀u ∈ SNoR x, - u < - x.
Assume _.
Apply minus_SNo_prop1 y Hy to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4.
Apply H4 to the current goal.
Assume H4: SNo (- y).
Assume H5: ∀u ∈ SNoL y, - y < - u.
Assume H6: ∀u ∈ SNoR y, - u < - y.
Assume _.
Apply SNoLtE x y Hx Hy Hxy to the current goal.
Let z be given.
Assume Hz: SNo z.
Assume Hz1: SNoLev z ∈ SNoLev x ∩ SNoLev y.
Assume Hz2: SNoEq_ (SNoLev z) z x.
Assume Hz3: SNoEq_ (SNoLev z) z y.
Assume Hz4: x < z.
Assume Hz5: z < y.
Assume Hz6: SNoLev z ∉ x.
Assume Hz7: SNoLev z ∈ y.
Apply binintersectE (SNoLev x) (SNoLev y) (SNoLev z) Hz1 to the current goal.
Assume Hz1x Hz1y.
We will prove - y < - x.
Apply SNoLt_tra (- y) (- z) (- x) H4 (SNo_minus_SNo z Hz) H1 to the current goal.
We will prove - y < - z.
Apply H5 z to the current goal.
We will prove z ∈ SNoL y.
We will prove z ∈ {x ∈ SNoS_ (SNoLev y)|x < y}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 z y Hz Hy Hz1y.
We will prove z < y.
An exact proof term for the current goal is Hz5.
We will prove - z < - x.
Apply H3 z to the current goal.
We will prove z ∈ SNoR x.
We will prove z ∈ {z ∈ SNoS_ (SNoLev x)|x < z}.
Apply SepI to the current goal.
We will prove z ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 z x Hz Hx Hz1x.
We will prove x < z.
An exact proof term for the current goal is Hz4.
Assume H7: SNoLev x ∈ SNoLev y.
Assume H8: SNoEq_ (SNoLev x) x y.
Assume H9: SNoLev x ∈ y.
Apply H5 x to the current goal.
We will prove x ∈ SNoL y.
We will prove x ∈ {x ∈ SNoS_ (SNoLev y)|x < y}.
Apply SepI to the current goal.
We will prove x ∈ SNoS_ (SNoLev y).
An exact proof term for the current goal is SNoS_I2 x y Hx Hy H7.
We will prove x < y.
An exact proof term for the current goal is Hxy.
Assume H7: SNoLev y ∈ SNoLev x.
Assume H8: SNoEq_ (SNoLev y) x y.
Assume H9: SNoLev y ∉ x.
We will prove - y < - x.
Apply H3 y to the current goal.
We will prove y ∈ SNoR x.
We will prove y ∈ {y ∈ SNoS_ (SNoLev x)|x < y}.
Apply SepI to the current goal.
We will prove y ∈ SNoS_ (SNoLev x).
An exact proof term for the current goal is SNoS_I2 y x Hy Hx H7.
We will prove x < y.
An exact proof term for the current goal is Hxy.
∎