We will prove continuous_map R R_standard_topology R R_standard_topology one_minus_fun.
Set Tx to be the term R_standard_topology.
Set S to be the term open_rays_subbasis R.
We prove the intermediate claim HTx: topology_on R Tx.
An exact proof term for the current goal is R_standard_topology_is_topology.
We prove the intermediate claim Hfun: function_on one_minus_fun R R.
Let t be given.
Assume HtR: t ∈ R.
An exact proof term for the current goal is (one_minus_fun_value_in_R t HtR).
We prove the intermediate claim HS: subbasis_on R S.
An exact proof term for the current goal is (open_rays_subbasis_is_subbasis R).
We prove the intermediate claim Hgen: generated_topology_from_subbasis R S = Tx.
rewrite the current goal using open_rays_subbasis_for_order_topology_R (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from left to right).
Use reflexivity.
rewrite the current goal using Hgen (from right to left) at position 2.
We prove the intermediate claim Hone_app: ∀t : set, t ∈ R → apply_fun one_minus_fun t = add_SNo 1 (minus_SNo t).
Let t be given.
Assume HtR: t ∈ R.
We prove the intermediate claim Hdef: one_minus_fun = graph R (λt0 : set ⇒ add_SNo 1 (minus_SNo t0)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ add_SNo 1 (minus_SNo t0)) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim Hflip_upper: ∀a t : set, a ∈ R → t ∈ R → (Rlt a (add_SNo 1 (minus_SNo t)) ↔ Rlt t (add_SNo 1 (minus_SNo a))).
Let a and t be given.
Assume HaR: a ∈ R.
Assume HtR: t ∈ R.
We will prove (Rlt a (add_SNo 1 (minus_SNo t)) ↔ Rlt t (add_SNo 1 (minus_SNo a))).
Apply iffI to the current goal.
Assume Hlt: Rlt a (add_SNo 1 (minus_SNo t)).
We will prove Rlt t (add_SNo 1 (minus_SNo a)).
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 HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim HsumS: SNo (add_SNo 1 (minus_SNo t)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo t) SNo_1 HmtS).
We prove the intermediate claim HltS: a < add_SNo 1 (minus_SNo t).
An exact proof term for the current goal is (RltE_lt a (add_SNo 1 (minus_SNo t)) Hlt).
We prove the intermediate claim H1: add_SNo a t < add_SNo (add_SNo 1 (minus_SNo t)) t.
An exact proof term for the current goal is (add_SNo_Lt1 a t (add_SNo 1 (minus_SNo t)) HaS HtS HsumS HltS).
We prove the intermediate claim HeqR: add_SNo (add_SNo 1 (minus_SNo t)) t = 1.
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo t) t SNo_1 HmtS HtS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv t HtS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
We prove the intermediate claim H2: add_SNo a t < 1.
rewrite the current goal using HeqR (from right to left).
An exact proof term for the current goal is H1.
We prove the intermediate claim H2c: add_SNo t a < 1.
rewrite the current goal using (add_SNo_com t a HtS HaS) (from left to right).
An exact proof term for the current goal is H2.
We prove the intermediate claim Hm1S: SNo (minus_SNo a).
An exact proof term for the current goal is HmaS.
We prove the intermediate claim H3: add_SNo (add_SNo t a) (minus_SNo a) < add_SNo 1 (minus_SNo a).
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo t a) (minus_SNo a) 1 (SNo_add_SNo t a HtS HaS) Hm1S SNo_1 H2c).
We prove the intermediate claim HeqL: add_SNo (add_SNo t a) (minus_SNo a) = t.
rewrite the current goal using (add_SNo_assoc t a (minus_SNo a) HtS HaS Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv a HaS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R t HtS).
We prove the intermediate claim H4: t < add_SNo 1 (minus_SNo a).
rewrite the current goal using HeqL (from right to left) at position 1.
An exact proof term for the current goal is H3.
We prove the intermediate claim Hflip_aR: add_SNo 1 (minus_SNo a) ∈ R.
We prove the intermediate claim HmaR: minus_SNo a ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo a) HmaR).
An exact proof term for the current goal is (RltI t (add_SNo 1 (minus_SNo a)) HtR Hflip_aR H4).
Assume Hlt: Rlt t (add_SNo 1 (minus_SNo a)).
We will prove Rlt a (add_SNo 1 (minus_SNo t)).
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 HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HmaS: SNo (minus_SNo a).
An exact proof term for the current goal is (SNo_minus_SNo a HaS).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim Hflip_aS: SNo (add_SNo 1 (minus_SNo a)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo a) SNo_1 HmaS).
We prove the intermediate claim HltS: t < add_SNo 1 (minus_SNo a).
An exact proof term for the current goal is (RltE_lt t (add_SNo 1 (minus_SNo a)) Hlt).
We prove the intermediate claim H1: add_SNo t a < add_SNo (add_SNo 1 (minus_SNo a)) a.
An exact proof term for the current goal is (add_SNo_Lt1 t a (add_SNo 1 (minus_SNo a)) HtS HaS Hflip_aS HltS).
We prove the intermediate claim HeqR: add_SNo (add_SNo 1 (minus_SNo a)) a = 1.
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo a) a SNo_1 HmaS HaS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv a HaS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
We prove the intermediate claim H2: add_SNo t a < 1.
rewrite the current goal using HeqR (from right to left).
An exact proof term for the current goal is H1.
We prove the intermediate claim H2c: add_SNo a t < 1.
rewrite the current goal using (add_SNo_com a t HaS HtS) (from left to right).
An exact proof term for the current goal is H2.
We prove the intermediate claim Hm1S: SNo (minus_SNo t).
An exact proof term for the current goal is HmtS.
We prove the intermediate claim H3: add_SNo (add_SNo a t) (minus_SNo t) < add_SNo 1 (minus_SNo t).
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo a t) (minus_SNo t) 1 (SNo_add_SNo a t HaS HtS) Hm1S SNo_1 H2c).
We prove the intermediate claim HeqL: add_SNo (add_SNo a t) (minus_SNo t) = a.
rewrite the current goal using (add_SNo_assoc a t (minus_SNo t) HaS HtS Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv t HtS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R a HaS).
We prove the intermediate claim H4: a < add_SNo 1 (minus_SNo t).
rewrite the current goal using HeqL (from right to left) at position 1.
An exact proof term for the current goal is H3.
We prove the intermediate claim Hflip_tR: add_SNo 1 (minus_SNo t) ∈ R.
We prove the intermediate claim HmtR: minus_SNo t ∈ R.
An exact proof term for the current goal is (real_minus_SNo t HtR).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo t) HmtR).
An exact proof term for the current goal is (RltI a (add_SNo 1 (minus_SNo t)) HaR Hflip_tR H4).
We prove the intermediate claim Hflip_lower: ∀t b : set, t ∈ R → b ∈ R → (Rlt (add_SNo 1 (minus_SNo t)) b ↔ Rlt (add_SNo 1 (minus_SNo b)) t).
Let t and b be given.
Assume HtR: t ∈ R.
Assume HbR: b ∈ R.
We will prove (Rlt (add_SNo 1 (minus_SNo t)) b ↔ Rlt (add_SNo 1 (minus_SNo b)) t).
Apply iffI to the current goal.
Assume Hlt: Rlt (add_SNo 1 (minus_SNo t)) b.
We will prove Rlt (add_SNo 1 (minus_SNo b)) t.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim HsumS: SNo (add_SNo 1 (minus_SNo t)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo t) SNo_1 HmtS).
We prove the intermediate claim HltS: add_SNo 1 (minus_SNo t) < b.
An exact proof term for the current goal is (RltE_lt (add_SNo 1 (minus_SNo t)) b Hlt).
We prove the intermediate claim H1: add_SNo (add_SNo 1 (minus_SNo t)) t < add_SNo b t.
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo 1 (minus_SNo t)) t b HsumS HtS HbS HltS).
We prove the intermediate claim HeqL: add_SNo (add_SNo 1 (minus_SNo t)) t = 1.
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo t) t SNo_1 HmtS HtS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv t HtS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
We prove the intermediate claim H2: 1 < add_SNo b t.
rewrite the current goal using HeqL (from right to left) at position 1.
An exact proof term for the current goal is H1.
We prove the intermediate claim H2c: 1 < add_SNo t b.
rewrite the current goal using (add_SNo_com t b HtS HbS) (from left to right).
An exact proof term for the current goal is H2.
We prove the intermediate claim Hm1S: SNo (minus_SNo b).
An exact proof term for the current goal is HmbS.
We prove the intermediate claim H3: add_SNo 1 (minus_SNo b) < add_SNo (add_SNo t b) (minus_SNo b).
An exact proof term for the current goal is (add_SNo_Lt1 1 (minus_SNo b) (add_SNo t b) SNo_1 Hm1S (SNo_add_SNo t b HtS HbS) H2c).
We prove the intermediate claim HeqR: add_SNo (add_SNo t b) (minus_SNo b) = t.
rewrite the current goal using (add_SNo_assoc t b (minus_SNo b) HtS HbS Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv b HbS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R t HtS).
We prove the intermediate claim H4: add_SNo 1 (minus_SNo b) < t.
rewrite the current goal using HeqR (from right to left).
An exact proof term for the current goal is H3.
We prove the intermediate claim Hflip_bR: add_SNo 1 (minus_SNo b) ∈ R.
We prove the intermediate claim HmbR: minus_SNo b ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo b) HmbR).
An exact proof term for the current goal is (RltI (add_SNo 1 (minus_SNo b)) t Hflip_bR HtR H4).
Assume Hlt: Rlt (add_SNo 1 (minus_SNo b)) t.
We will prove Rlt (add_SNo 1 (minus_SNo t)) b.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HbS: SNo b.
An exact proof term for the current goal is (real_SNo b HbR).
We prove the intermediate claim HmtS: SNo (minus_SNo t).
An exact proof term for the current goal is (SNo_minus_SNo t HtS).
We prove the intermediate claim HmbS: SNo (minus_SNo b).
An exact proof term for the current goal is (SNo_minus_SNo b HbS).
We prove the intermediate claim HsumS: SNo (add_SNo 1 (minus_SNo b)).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo b) SNo_1 HmbS).
We prove the intermediate claim HltS: add_SNo 1 (minus_SNo b) < t.
An exact proof term for the current goal is (RltE_lt (add_SNo 1 (minus_SNo b)) t Hlt).
We prove the intermediate claim H1: add_SNo (add_SNo 1 (minus_SNo b)) b < add_SNo t b.
An exact proof term for the current goal is (add_SNo_Lt1 (add_SNo 1 (minus_SNo b)) b t HsumS HbS HtS HltS).
We prove the intermediate claim HeqL: add_SNo (add_SNo 1 (minus_SNo b)) b = 1.
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo b) b SNo_1 HmbS HbS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv b HbS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R 1 SNo_1).
We prove the intermediate claim H2: 1 < add_SNo t b.
rewrite the current goal using HeqL (from right to left) at position 1.
An exact proof term for the current goal is H1.
We prove the intermediate claim H2c: 1 < add_SNo b t.
rewrite the current goal using (add_SNo_com t b HtS HbS) (from right to left).
An exact proof term for the current goal is H2.
We prove the intermediate claim Hm1S: SNo (minus_SNo t).
An exact proof term for the current goal is HmtS.
We prove the intermediate claim H3: add_SNo 1 (minus_SNo t) < add_SNo (add_SNo b t) (minus_SNo t).
An exact proof term for the current goal is (add_SNo_Lt1 1 (minus_SNo t) (add_SNo b t) SNo_1 Hm1S (SNo_add_SNo b t HbS HtS) H2c).
We prove the intermediate claim HeqR: add_SNo (add_SNo b t) (minus_SNo t) = b.
rewrite the current goal using (add_SNo_assoc b t (minus_SNo t) HbS HtS Hm1S) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv t HtS) (from left to right).
An exact proof term for the current goal is (add_SNo_0R b HbS).
We prove the intermediate claim H4: add_SNo 1 (minus_SNo t) < b.
rewrite the current goal using HeqR (from right to left).
An exact proof term for the current goal is H3.
We prove the intermediate claim Hflip_tR: add_SNo 1 (minus_SNo t) ∈ R.
We prove the intermediate claim HmtR: minus_SNo t ∈ R.
An exact proof term for the current goal is (real_minus_SNo t HtR).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo t) HmtR).
An exact proof term for the current goal is (RltI (add_SNo 1 (minus_SNo t)) b Hflip_tR HbR H4).
We prove the intermediate claim HpreS: ∀s : set, s ∈ S → preimage_of R one_minus_fun s ∈ Tx.
Let s be given.
Assume HsS: s ∈ S.
We will prove preimage_of R one_minus_fun s ∈ Tx.
Apply (binunionE' ({I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} ∪ {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b}) {R} s (preimage_of R one_minus_fun s ∈ Tx)) to the current goal.
Assume Hs0: s ∈ ({I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} ∪ {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b}).
Apply (binunionE' {I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a} {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b} s (preimage_of R one_minus_fun s ∈ Tx)) to the current goal.
Assume Hsu: s ∈ {I ∈ 𝒫 R|∃a ∈ R, I = open_ray_upper R a}.
We prove the intermediate claim Hex: ∃a ∈ R, s = open_ray_upper R a.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃a ∈ R, I0 = open_ray_upper R a) s Hsu).
Apply Hex to the current goal.
Let a be given.
Assume Hacore.
Apply Hacore to the current goal.
Assume HaR: a ∈ R.
Assume Hseq: s = open_ray_upper R a.
Set c to be the term add_SNo 1 (minus_SNo a).
We prove the intermediate claim HcR: c ∈ R.
We prove the intermediate claim HmaR: minus_SNo a ∈ R.
An exact proof term for the current goal is (real_minus_SNo a HaR).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo a) HmaR).
We prove the intermediate claim Hcdef: c = add_SNo 1 (minus_SNo a).
Use reflexivity.
We prove the intermediate claim HpreEq: preimage_of R one_minus_fun (open_ray_upper R a) = open_ray_lower R c.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of R one_minus_fun (open_ray_upper R a).
We will prove t ∈ open_ray_lower R c.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun one_minus_fun x0 ∈ open_ray_upper R a) t Ht).
We prove the intermediate claim Himg: apply_fun one_minus_fun t ∈ open_ray_upper R a.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun one_minus_fun x0 ∈ open_ray_upper R a) t Ht).
We prove the intermediate claim Hrel: order_rel R a (apply_fun one_minus_fun t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R a x0) (apply_fun one_minus_fun t) Himg).
We prove the intermediate claim Hrlt: Rlt a (apply_fun one_minus_fun t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt a (apply_fun one_minus_fun t) Hrel).
We prove the intermediate claim Hrlt2: Rlt a (add_SNo 1 (minus_SNo t)).
rewrite the current goal using (Hone_app t HtR) (from right to left).
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim Hrlt3: Rlt t (add_SNo 1 (minus_SNo a)).
An exact proof term for the current goal is (iffEL (Rlt a (add_SNo 1 (minus_SNo t))) (Rlt t (add_SNo 1 (minus_SNo a))) (Hflip_upper a t HaR HtR) Hrlt2).
We prove the intermediate claim Hrlt4: Rlt t c.
rewrite the current goal using Hcdef (from left to right).
An exact proof term for the current goal is Hrlt3.
We prove the intermediate claim Hrel4: order_rel R t c.
An exact proof term for the current goal is (Rlt_implies_order_rel_R t c Hrlt4).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 c) t HtR Hrel4).
Let t be given.
Assume Ht: t ∈ open_ray_lower R c.
We will prove t ∈ preimage_of R one_minus_fun (open_ray_upper R a).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R x0 c) t Ht).
We prove the intermediate claim Hrel: order_rel R t c.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 c) t Ht).
We prove the intermediate claim Hrlt: Rlt t c.
An exact proof term for the current goal is (order_rel_R_implies_Rlt t c Hrel).
We prove the intermediate claim Hrlt2: Rlt t (add_SNo 1 (minus_SNo a)).
rewrite the current goal using Hcdef (from right to left).
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim Hrlt3: Rlt a (add_SNo 1 (minus_SNo t)).
An exact proof term for the current goal is (iffER (Rlt a (add_SNo 1 (minus_SNo t))) (Rlt t (add_SNo 1 (minus_SNo a))) (Hflip_upper a t HaR HtR) Hrlt2).
We prove the intermediate claim Ht0: t ∈ preimage_of R one_minus_fun (open_ray_upper R a).
We prove the intermediate claim Hpredef: preimage_of R one_minus_fun (open_ray_upper R a) = {x0 ∈ R|apply_fun one_minus_fun x0 ∈ open_ray_upper R a}.
Use reflexivity.
rewrite the current goal using Hpredef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HtR.
We prove the intermediate claim HimgR: apply_fun one_minus_fun t ∈ R.
An exact proof term for the current goal is (Hfun t HtR).
We prove the intermediate claim HimgEq: apply_fun one_minus_fun t = add_SNo 1 (minus_SNo t).
An exact proof term for the current goal is (Hone_app t HtR).
We prove the intermediate claim Hrlt4: Rlt a (apply_fun one_minus_fun t).
rewrite the current goal using HimgEq (from left to right).
An exact proof term for the current goal is Hrlt3.
We prove the intermediate claim Hrel4: order_rel R a (apply_fun one_minus_fun t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R a (apply_fun one_minus_fun t) Hrlt4).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R a x0) (apply_fun one_minus_fun t) HimgR Hrel4).
An exact proof term for the current goal is Ht0.
rewrite the current goal using Hseq (from left to right).
rewrite the current goal using HpreEq (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_lower R c ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R c HcR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_lower R c) HsRay).
Assume Hsl: s ∈ {I ∈ 𝒫 R|∃b ∈ R, I = open_ray_lower R b}.
We prove the intermediate claim Hex: ∃b ∈ R, s = open_ray_lower R b.
An exact proof term for the current goal is (SepE2 (𝒫 R) (λI0 : set ⇒ ∃b ∈ R, I0 = open_ray_lower R b) s Hsl).
Apply Hex to the current goal.
Let b be given.
Assume Hbcore.
Apply Hbcore to the current goal.
Assume HbR: b ∈ R.
Assume Hseq: s = open_ray_lower R b.
Set c to be the term add_SNo 1 (minus_SNo b).
We prove the intermediate claim HcR: c ∈ R.
We prove the intermediate claim HmbR: minus_SNo b ∈ R.
An exact proof term for the current goal is (real_minus_SNo b HbR).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo b) HmbR).
We prove the intermediate claim Hcdef: c = add_SNo 1 (minus_SNo b).
Use reflexivity.
We prove the intermediate claim HpreEq: preimage_of R one_minus_fun (open_ray_lower R b) = open_ray_upper R c.
Apply set_ext to the current goal.
Let t be given.
Assume Ht: t ∈ preimage_of R one_minus_fun (open_ray_lower R b).
We will prove t ∈ open_ray_upper R c.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ apply_fun one_minus_fun x0 ∈ open_ray_lower R b) t Ht).
We prove the intermediate claim Himg: apply_fun one_minus_fun t ∈ open_ray_lower R b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ apply_fun one_minus_fun x0 ∈ open_ray_lower R b) t Ht).
We prove the intermediate claim Hrel: order_rel R (apply_fun one_minus_fun t) b.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 b) (apply_fun one_minus_fun t) Himg).
We prove the intermediate claim Hrlt: Rlt (apply_fun one_minus_fun t) b.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun one_minus_fun t) b Hrel).
We prove the intermediate claim Hrlt2: Rlt (add_SNo 1 (minus_SNo t)) b.
rewrite the current goal using (Hone_app t HtR) (from right to left).
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim Hrlt3: Rlt (add_SNo 1 (minus_SNo b)) t.
An exact proof term for the current goal is (iffEL (Rlt (add_SNo 1 (minus_SNo t)) b) (Rlt (add_SNo 1 (minus_SNo b)) t) (Hflip_lower t b HtR HbR) Hrlt2).
We prove the intermediate claim Hrlt4: Rlt c t.
rewrite the current goal using Hcdef (from left to right).
An exact proof term for the current goal is Hrlt3.
We prove the intermediate claim Hrel4: order_rel R c t.
An exact proof term for the current goal is (Rlt_implies_order_rel_R c t Hrlt4).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R c x0) t HtR Hrel4).
Let t be given.
Assume Ht: t ∈ open_ray_upper R c.
We will prove t ∈ preimage_of R one_minus_fun (open_ray_lower R b).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R c x0) t Ht).
We prove the intermediate claim Hrel: order_rel R c t.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R c x0) t Ht).
We prove the intermediate claim Hrlt: Rlt c t.
An exact proof term for the current goal is (order_rel_R_implies_Rlt c t Hrel).
We prove the intermediate claim Hrlt2: Rlt (add_SNo 1 (minus_SNo b)) t.
rewrite the current goal using Hcdef (from right to left).
An exact proof term for the current goal is Hrlt.
We prove the intermediate claim Hrlt3: Rlt (add_SNo 1 (minus_SNo t)) b.
An exact proof term for the current goal is (iffER (Rlt (add_SNo 1 (minus_SNo t)) b) (Rlt (add_SNo 1 (minus_SNo b)) t) (Hflip_lower t b HtR HbR) Hrlt2).
We prove the intermediate claim Hpredef: preimage_of R one_minus_fun (open_ray_lower R b) = {x0 ∈ R|apply_fun one_minus_fun x0 ∈ open_ray_lower R b}.
Use reflexivity.
rewrite the current goal using Hpredef (from left to right).
Apply SepI to the current goal.
An exact proof term for the current goal is HtR.
We prove the intermediate claim HimgR: apply_fun one_minus_fun t ∈ R.
An exact proof term for the current goal is (Hfun t HtR).
We prove the intermediate claim HimgEq: apply_fun one_minus_fun t = add_SNo 1 (minus_SNo t).
An exact proof term for the current goal is (Hone_app t HtR).
We prove the intermediate claim Hrlt4: Rlt (apply_fun one_minus_fun t) b.
rewrite the current goal using HimgEq (from left to right).
An exact proof term for the current goal is Hrlt3.
We prove the intermediate claim Hrel4: order_rel R (apply_fun one_minus_fun t) b.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun one_minus_fun t) b Hrlt4).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 b) (apply_fun one_minus_fun t) HimgR Hrel4).
rewrite the current goal using Hseq (from left to right).
rewrite the current goal using HpreEq (from left to right).
rewrite the current goal using standard_topology_is_order_topology (from right to left).
We prove the intermediate claim HsRay: open_ray_upper R c ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_in_open_rays_subbasis R c HcR).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_upper R c) HsRay).
An exact proof term for the current goal is Hs0.
Assume HsR: s ∈ {R}.
We prove the intermediate claim Hseq: s = R.
An exact proof term for the current goal is (SingE R s HsR).
rewrite the current goal using Hseq (from left to right).
We prove the intermediate claim Heq: preimage_of R one_minus_fun R = R.
An exact proof term for the current goal is (preimage_of_whole R R one_minus_fun Hfun).
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (topology_has_X R Tx HTx).
An exact proof term for the current goal is HsS.
An exact proof term for the current goal is (continuous_map_from_subbasis R Tx R S one_minus_fun HTx Hfun HS HpreS).
∎