Let n be given.
Assume HnO: n ∈ ω.
Set X to be the term setprod 2 ω.
Set b to be the term (1,ordsucc n).
Set pred to be the term (1,n).
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 1 (ordsucc n) In_1_2 (omega_ordsucc n HnO)).
We prove the intermediate claim HpredX: pred ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 1 n In_1_2 HnO).
We prove the intermediate claim Hso: simply_ordered_set X.
An exact proof term for the current goal is simply_ordered_set_setprod_2_omega.
We will prove X ∖ open_ray_lower X b = open_ray_upper X pred.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ X ∖ open_ray_lower X b.
We will prove y ∈ open_ray_upper X pred.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (setminusE1 X (open_ray_lower X b) y Hy).
We prove the intermediate claim HyNot: y ∉ open_ray_lower X b.
An exact proof term for the current goal is (setminusE2 X (open_ray_lower X b) y Hy).
We prove the intermediate claim HupDef: open_ray_upper X pred = {y0 ∈ X|order_rel X pred y0}.
Use reflexivity.
rewrite the current goal using HupDef (from left to right).
Apply (SepI X (λy0 : set ⇒ order_rel X pred y0) y HyX) to the current goal.
We prove the intermediate claim Hpredb: order_rel X pred b.
We prove the intermediate claim H11: 1 = 1.
Use reflexivity.
An exact proof term for the current goal is (order_rel_setprod_2_omega_intro 1 n 1 (ordsucc n) In_1_2 HnO In_1_2 (omega_ordsucc n HnO) (orIR (1 ∈ 1) (1 = 1 ∧ n ∈ ordsucc n) (andI (1 = 1) (n ∈ ordsucc n) H11 (ordsuccI2 n)))).
Apply (order_rel_trichotomy_or_impred X y pred Hso HyX HpredX (order_rel X pred y)) to the current goal.
Assume Hyp: order_rel X y pred.
Apply FalseE to the current goal.
We prove the intermediate claim Hyb: order_rel X y b.
An exact proof term for the current goal is (order_rel_trans X y pred b Hso HyX HpredX HbX Hyp Hpredb).
We prove the intermediate claim HyInLow: y ∈ open_ray_lower X b.
We prove the intermediate claim HlowDef: open_ray_lower X b = {y0 ∈ X|order_rel X y0 b}.
Use reflexivity.
rewrite the current goal using HlowDef (from left to right).
Apply (SepI X (λy0 : set ⇒ order_rel X y0 b) y HyX) to the current goal.
An exact proof term for the current goal is Hyb.
An exact proof term for the current goal is (HyNot HyInLow).
Assume Hey: y = pred.
Apply FalseE to the current goal.
We prove the intermediate claim HyInLow: y ∈ open_ray_lower X b.
rewrite the current goal using Hey (from left to right).
We prove the intermediate claim HlowDef: open_ray_lower X b = {y0 ∈ X|order_rel X y0 b}.
Use reflexivity.
rewrite the current goal using HlowDef (from left to right).
Apply (SepI X (λy0 : set ⇒ order_rel X y0 b) pred HpredX) to the current goal.
An exact proof term for the current goal is Hpredb.
An exact proof term for the current goal is (HyNot HyInLow).
Assume Hpy: order_rel X pred y.
An exact proof term for the current goal is Hpy.
Let y be given.
Assume Hy: y ∈ open_ray_upper X pred.
We will prove y ∈ X ∖ open_ray_lower X b.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ order_rel X pred y0) y Hy).
We prove the intermediate claim Hpy: order_rel X pred y.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ order_rel X pred y0) y Hy).
Apply (setminusI X (open_ray_lower X b) y HyX) to the current goal.
Assume HyLow: y ∈ open_ray_lower X b.
We prove the intermediate claim Hyb: order_rel X y b.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ order_rel X y0 b) y HyLow).
An exact proof term for the current goal is (no_point_between_setprod_2_omega_1n_1succn n y HnO HyX Hpy Hyb).
∎