Let k be given.
Assume HkO: k ∈ ω.
Set X to be the term setprod 2 ω.
Set a to be the term (0,k).
Set s to be the term (0,ordsucc k).
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 k In_0_2 HkO).
We prove the intermediate claim HsX: s ∈ X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 (ordsucc k) In_0_2 (omega_ordsucc k HkO)).
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_upper X a = open_ray_lower X s.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ X ∖ open_ray_upper X a.
We will prove y ∈ open_ray_lower X s.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (setminusE1 X (open_ray_upper X a) y Hy).
We prove the intermediate claim HyNot: y ∉ open_ray_upper X a.
An exact proof term for the current goal is (setminusE2 X (open_ray_upper X a) y Hy).
We prove the intermediate claim HlowDef: open_ray_lower X s = {y0 ∈ X|order_rel X y0 s}.
Use reflexivity.
rewrite the current goal using HlowDef (from left to right).
Apply (SepI X (λy0 : set ⇒ order_rel X y0 s) y HyX) to the current goal.
We prove the intermediate claim Haks: order_rel X a s.
We prove the intermediate claim Hrel: order_rel (setprod 2 ω) (0,k) (0,ordsucc k).
An exact proof term for the current goal is (order_rel_setprod_2_omega_0k_0succk k HkO).
An exact proof term for the current goal is Hrel.
Apply (order_rel_trichotomy_or_impred X y s Hso HyX HsX (order_rel X y s)) to the current goal.
Assume Hys: order_rel X y s.
An exact proof term for the current goal is Hys.
Assume Hey: y = s.
Apply FalseE to the current goal.
We prove the intermediate claim HsinUp: s ∈ open_ray_upper X a.
We prove the intermediate claim HupDef: open_ray_upper X a = {y0 ∈ X|order_rel X a y0}.
Use reflexivity.
rewrite the current goal using HupDef (from left to right).
Apply (SepI X (λy0 : set ⇒ order_rel X a y0) s HsX) to the current goal.
An exact proof term for the current goal is Haks.
We prove the intermediate claim HyInUp: y ∈ open_ray_upper X a.
rewrite the current goal using Hey (from left to right).
An exact proof term for the current goal is HsinUp.
An exact proof term for the current goal is (HyNot HyInUp).
Assume Hsy: order_rel X s y.
Apply FalseE to the current goal.
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (order_rel_trans X a s y Hso HaX HsX HyX Haks Hsy).
We prove the intermediate claim HyInUp: y ∈ open_ray_upper X a.
We prove the intermediate claim HupDef: open_ray_upper X a = {y0 ∈ X|order_rel X a y0}.
Use reflexivity.
rewrite the current goal using HupDef (from left to right).
Apply (SepI X (λy0 : set ⇒ order_rel X a y0) y HyX) to the current goal.
An exact proof term for the current goal is Hay.
An exact proof term for the current goal is (HyNot HyInUp).
Let y be given.
Assume Hy: y ∈ open_ray_lower X s.
We will prove y ∈ X ∖ open_ray_upper X a.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (SepE1 X (λy0 : set ⇒ order_rel X y0 s) y Hy).
We prove the intermediate claim Hys: order_rel X y s.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ order_rel X y0 s) y Hy).
Apply (setminusI X (open_ray_upper X a) y HyX) to the current goal.
Assume HyUp: y ∈ open_ray_upper X a.
We prove the intermediate claim Hay: order_rel X a y.
An exact proof term for the current goal is (SepE2 X (λy0 : set ⇒ order_rel X a y0) y HyUp).
An exact proof term for the current goal is (no_point_between_setprod_2_omega_0k_0succk k y HkO HyX Hay Hys).
∎