Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ closure_of R R_ray_topology K_set.
We will prove x ∈ R_nonneg_set.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ ∀U : set, U ∈ R_ray_topology → x0 ∈ U → U ∩ K_set ≠ Empty) x Hx).
We prove the intermediate claim Hcl: ∀U : set, U ∈ R_ray_topology → x ∈ U → U ∩ K_set ≠ Empty.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ ∀U : set, U ∈ R_ray_topology → x0 ∈ U → U ∩ K_set ≠ Empty) x Hx).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim H0lex: 0 ≤ x.
Apply (SNoLt_trichotomy_or_impred x 0 HxS SNo_0 (0 ≤ x)) to the current goal.
Assume Hxlt0: x < 0.
Apply FalseE to the current goal.
Set U0 to be the term {y ∈ R|Rlt y 0}.
We prove the intermediate claim HU0pow: U0 ∈ 𝒫 R.
Apply PowerI to the current goal.
Let y be given.
Assume Hy: y ∈ U0.
An exact proof term for the current goal is (SepE1 R (λy0 : set ⇒ Rlt y0 0) y Hy).
We prove the intermediate claim HU0disj: U0 = Empty ∨ U0 = R ∨ (∃a ∈ R, U0 = {y ∈ R|Rlt y a}).
Apply orIR to the current goal.
We use 0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is real_0.
Use reflexivity.
We prove the intermediate claim HU0top: U0 ∈ R_ray_topology.
An exact proof term for the current goal is (SepI (𝒫 R) (λU : set ⇒ U = Empty ∨ U = R ∨ (∃a ∈ R, U = {y ∈ R|Rlt y a})) U0 HU0pow HU0disj).
We prove the intermediate claim HxU0: x ∈ U0.
We prove the intermediate claim HxRlt0: Rlt x 0.
An exact proof term for the current goal is (RltI x 0 HxR real_0 Hxlt0).
An exact proof term for the current goal is (SepI R (λy : set ⇒ Rlt y 0) x HxR HxRlt0).
We prove the intermediate claim Hne: U0 ∩ K_set ≠ Empty.
An exact proof term for the current goal is (Hcl U0 HU0top HxU0).
We prove the intermediate claim Hempty: U0 ∩ K_set = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ U0 ∩ K_set.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU0: z ∈ U0.
An exact proof term for the current goal is (binintersectE1 U0 K_set z Hz).
We prove the intermediate claim HzK: z ∈ K_set.
An exact proof term for the current goal is (binintersectE2 U0 K_set z Hz).
We prove the intermediate claim Hzlt0: Rlt z 0.
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ Rlt y0 0) z HzU0).
Apply (ReplE_impred (ω ∖ {0}) (λn : set ⇒ inv_nat n) z HzK False) to the current goal.
Let n be given.
Assume HnIn: n ∈ ω ∖ {0}.
Assume Hzeq: z = inv_nat n.
We prove the intermediate claim Hzpos: Rlt 0 z.
rewrite the current goal using Hzeq (from left to right).
An exact proof term for the current goal is (inv_nat_pos n HnIn).
We prove the intermediate claim H00: Rlt 0 0.
An exact proof term for the current goal is (Rlt_tra 0 z 0 Hzpos Hzlt0).
An exact proof term for the current goal is ((not_Rlt_refl 0 real_0) H00).
An exact proof term for the current goal is (Hne Hempty).
Assume Hx0: x = 0.
rewrite the current goal using Hx0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
Assume H0ltx: 0 < x.
An exact proof term for the current goal is (SNoLtLe 0 x H0ltx).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ 0 ≤ x0) x HxR H0lex).
Let x be given.
Assume Hx: x ∈ R_nonneg_set.
We will prove x ∈ closure_of R R_ray_topology K_set.
We prove the intermediate claim HxR: x ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ 0 ≤ x0) x Hx).
We prove the intermediate claim H0lex: 0 ≤ x.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ 0 ≤ x0) x Hx).
We prove the intermediate claim HxS: SNo x.
An exact proof term for the current goal is (real_SNo x HxR).
We prove the intermediate claim Hcl: ∀U : set, U ∈ R_ray_topology → x ∈ U → U ∩ K_set ≠ Empty.
Let U be given.
Assume HU: U ∈ R_ray_topology.
Assume HxU: x ∈ U.
We will prove U ∩ K_set ≠ Empty.
We prove the intermediate claim HUcases: U = Empty ∨ U = R ∨ (∃a ∈ R, U = {y ∈ R|Rlt y a}).
An exact proof term for the current goal is (SepE2 (𝒫 R) (λU0 : set ⇒ U0 = Empty ∨ U0 = R ∨ (∃a0 ∈ R, U0 = {y ∈ R|Rlt y a0})) U HU).
Apply (HUcases (U ∩ K_set ≠ Empty)) to the current goal.
Assume HUR: U = Empty ∨ U = R.
Apply (HUR (U ∩ K_set ≠ Empty)) to the current goal.
Assume HUe: U = Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HxE: x ∈ Empty.
rewrite the current goal using HUe (from right to left).
An exact proof term for the current goal is HxU.
An exact proof term for the current goal is (EmptyE x HxE).
Assume HUeqR: U = R.
We prove the intermediate claim Hexy: ∃y : set, y ∈ halfopen_interval_left 0 1 ∧ y ∈ K_set.
An exact proof term for the current goal is (K_set_meets_lower_limit_neighborhood_0 0 1 real_0 real_1 (not_Rlt_refl 0 real_0) (RltI 0 1 real_0 real_1 SNoLt_0_1)).
Apply Hexy to the current goal.
Let y be given.
Assume Hypair.
We prove the intermediate claim HyK: y ∈ K_set.
An exact proof term for the current goal is (andER (y ∈ halfopen_interval_left 0 1) (y ∈ K_set) Hypair).
We prove the intermediate claim HyU: y ∈ U.
rewrite the current goal using HUeqR (from left to right).
An exact proof term for the current goal is (K_set_Subq_R y HyK).
We prove the intermediate claim HyInt: y ∈ U ∩ K_set.
An exact proof term for the current goal is (binintersectI U K_set y HyU HyK).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ K_set) y HyInt).
Assume Hex: ∃a ∈ R, U = {y ∈ R|Rlt y a}.
Apply Hex to the current goal.
Let a be given.
Assume Hapair.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is (andEL (a ∈ R) (U = {y ∈ R|Rlt y a}) Hapair).
We prove the intermediate claim HUeq: U = {y ∈ R|Rlt y a}.
An exact proof term for the current goal is (andER (a ∈ R) (U = {y ∈ R|Rlt y a}) Hapair).
We prove the intermediate claim HxUa: x ∈ {y ∈ R|Rlt y a}.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HxU.
We prove the intermediate claim Hxlt: Rlt x a.
An exact proof term for the current goal is (SepE2 R (λy0 : set ⇒ Rlt y0 a) x HxUa).
We prove the intermediate claim HxltS: x < a.
An exact proof term for the current goal is (RltE_lt x a Hxlt).
We prove the intermediate claim HaS: SNo a.
An exact proof term for the current goal is (real_SNo a HaR).
We prove the intermediate claim H0ltaS: 0 < a.
An exact proof term for the current goal is (SNoLeLt_tra 0 x a SNo_0 HxS HaS H0lex HxltS).
We prove the intermediate claim H0lta: Rlt 0 a.
An exact proof term for the current goal is (RltI 0 a real_0 HaR H0ltaS).
We prove the intermediate claim Hexy: ∃y : set, y ∈ halfopen_interval_left 0 a ∧ y ∈ K_set.
An exact proof term for the current goal is (K_set_meets_lower_limit_neighborhood_0 0 a real_0 HaR (not_Rlt_refl 0 real_0) H0lta).
Apply Hexy to the current goal.
Let y be given.
Assume Hypair.
We prove the intermediate claim Hyhalf: y ∈ halfopen_interval_left 0 a.
An exact proof term for the current goal is (andEL (y ∈ halfopen_interval_left 0 a) (y ∈ K_set) Hypair).
We prove the intermediate claim HyK: y ∈ K_set.
An exact proof term for the current goal is (andER (y ∈ halfopen_interval_left 0 a) (y ∈ K_set) Hypair).
We prove the intermediate claim Hylt: Rlt y a.
An exact proof term for the current goal is (andER (¬ (Rlt y 0)) (Rlt y a) (SepE2 R (λy0 : set ⇒ ¬ (Rlt y0 0) ∧ Rlt y0 a) y Hyhalf)).
We prove the intermediate claim HyU: y ∈ U.
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (SepI R (λy0 : set ⇒ Rlt y0 a) y (K_set_Subq_R y HyK) Hylt).
We prove the intermediate claim HyInt: y ∈ U ∩ K_set.
An exact proof term for the current goal is (binintersectI U K_set y HyU HyK).
An exact proof term for the current goal is (elem_implies_nonempty (U ∩ K_set) y HyInt).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ ∀U : set, U ∈ R_ray_topology → x0 ∈ U → U ∩ K_set ≠ Empty) x HxR Hcl).
∎