Let y be given.

Assume Hy: y ∈ open_ray_lower X s.

We will prove y ∈ {(0,0)}.

We prove the intermediate claim HlowDef: open_ray_lower X s = {y0 ∈ X|order_rel X y0 s}.

Use reflexivity.

We prove the intermediate claim HySep: y ∈ {y0 ∈ X|order_rel X y0 s}.

rewrite the current goal using HlowDef (from right to left).

An exact proof term for the current goal is Hy.

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 HySep).

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 HySep).

Apply (order_rel_setprod_2_omega_unfold y s Hys) to the current goal.

Let i be given.

Assume HiPair.

Apply HiPair to the current goal.

Let m be given.

Assume HmPair.

Apply HmPair to the current goal.

Let j be given.

Assume HjPair.

Apply HjPair to the current goal.

Let n be given.

Assume Hcore: (i ∈ 2 ∧ m ∈ ω ∧ j ∈ 2 ∧ n ∈ ω ∧ y = (i,m) ∧ s = (j,n) ∧ (i ∈ j ∨ (i = j ∧ m ∈ n))).

Apply (and7E (i ∈ 2) (m ∈ ω) (j ∈ 2) (n ∈ ω) (y = (i,m)) (s = (j,n)) (i ∈ j ∨ (i = j ∧ m ∈ n)) Hcore (y ∈ {(0,0)})) to the current goal.

Assume Hi2 HmO Hj2 HnO Hyeq Hseq Hlex.

We prove the intermediate claim HsEq: s = (0,1).

Use reflexivity.

We prove the intermediate claim Heq01jn: (0,1) = (j,n).

We will prove (0,1) = (j,n).

rewrite the current goal using HsEq (from right to left).

An exact proof term for the current goal is Hseq.

We prove the intermediate claim H0j: 0 = j.

An exact proof term for the current goal is (pair_eq_fst 0 1 j n Heq01jn).

We prove the intermediate claim Hj0: j = 0.

Use symmetry.

An exact proof term for the current goal is H0j.

We prove the intermediate claim H1n: 1 = n.

An exact proof term for the current goal is (pair_eq_snd 0 1 j n Heq01jn).

We prove the intermediate claim Hn1: n = 1.

Use symmetry.

An exact proof term for the current goal is H1n.

Apply Hlex to the current goal.

Assume Hij: i ∈ j.

Apply FalseE to the current goal.

We prove the intermediate claim HiIn0: i ∈ 0.

We will prove i ∈ 0.

rewrite the current goal using Hj0 (from right to left).

An exact proof term for the current goal is Hij.

An exact proof term for the current goal is (EmptyE i HiIn0).

Assume Hmn: i = j ∧ m ∈ n.

We prove the intermediate claim HijEq: i = j.

An exact proof term for the current goal is (andEL (i = j) (m ∈ n) Hmn).

We prove the intermediate claim HmInN: m ∈ n.

An exact proof term for the current goal is (andER (i = j) (m ∈ n) Hmn).

We prove the intermediate claim Hi0: i = 0.

We will prove i = 0.

rewrite the current goal using HijEq (from left to right).

An exact proof term for the current goal is Hj0.

We prove the intermediate claim HmIn1: m ∈ 1.

We will prove m ∈ 1.

rewrite the current goal using Hn1 (from right to left).

An exact proof term for the current goal is HmInN.

Apply (ordsuccE 0 m HmIn1 (y ∈ {(0,0)})) to the current goal.

Assume HmIn0: m ∈ 0.

Apply FalseE to the current goal.

An exact proof term for the current goal is (EmptyE m HmIn0).

Assume Hm0: m = 0.

We prove the intermediate claim HyEq00: y = (0,0).

We will prove y = (0,0).

rewrite the current goal using Hyeq (from left to right).

rewrite the current goal using Hi0 (from left to right).

rewrite the current goal using Hm0 (from left to right).

Use reflexivity.

rewrite the current goal using HyEq00 (from left to right).

An exact proof term for the current goal is (SingI (0,0)).

Let y be given.

Assume Hy: y ∈ {(0,0)}.

We will prove y ∈ open_ray_lower X s.

We prove the intermediate claim HyEq00: y = (0,0).

An exact proof term for the current goal is (SingE (0,0) y Hy).

We prove the intermediate claim H0O: 0 ∈ ω.

An exact proof term for the current goal is (nat_p_omega 0 nat_0).

We prove the intermediate claim HyX: y ∈ X.

We will prove y ∈ X.

rewrite the current goal using HyEq00 (from left to right).

An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma 2 ω 0 0 In_0_2 H0O).

We prove the intermediate claim Hys: order_rel X y s.

We will prove order_rel X y s.

rewrite the current goal using HyEq00 (from left to right).

We prove the intermediate claim HsEq: s = (0,1).

Use reflexivity.

rewrite the current goal using HsEq (from left to right).

We prove the intermediate claim Hsucc0eq1: ordsucc 0 = 1.

Use reflexivity.

rewrite the current goal using Hsucc0eq1 (from right to left).

An exact proof term for the current goal is (order_rel_setprod_2_omega_0k_0succk 0 H0O).

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).

An exact proof term for the current goal is (SepI X (λy0 : set ⇒ order_rel X y0 s) y HyX Hys).