We will prove open_ray_lower ω 1 = {0}.
Apply set_ext to the current goal.
Let y be given.
Assume Hy: y ∈ open_ray_lower ω 1.
We will prove y ∈ {0}.
We prove the intermediate claim Hyrel: order_rel ω y 1.
An exact proof term for the current goal is (SepE2 ω (λy0 : set ⇒ order_rel ω y0 1) y Hy).
We prove the intermediate claim Hymem: y ∈ 1.
An exact proof term for the current goal is (order_rel_omega_implies_mem y 1 Hyrel).
Apply (ordsuccE 0 y Hymem) to the current goal.
Assume Hy0: y ∈ 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (EmptyE y Hy0).
Assume Heq: y = 0.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI 0).
Let y be given.
Assume Hy: y ∈ {0}.
We will prove y ∈ open_ray_lower ω 1.
We prove the intermediate claim Heq: y = 0.
An exact proof term for the current goal is (SingE 0 y Hy).
rewrite the current goal using Heq (from left to right).
We prove the intermediate claim H0omega: 0 ∈ ω.
An exact proof term for the current goal is (nat_p_omega 0 nat_0).
We prove the intermediate claim Hdef: open_ray_lower ω 1 = {y0 ∈ ω|order_rel ω y0 1}.
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
Apply (SepI ω (λy0 : set ⇒ order_rel ω y0 1) 0 H0omega) to the current goal.
An exact proof term for the current goal is (mem_implies_order_rel_omega 0 1 In_0_1).
∎