Let b be given.
Assume HbR: b ∈ R.
Assume Hm1ltb: Rlt (minus_SNo 1) b.
Assume Hblt1: Rlt b 1.
We will prove preimage_of R bounded_transform_phi (open_ray_lower R b) ∈ R_standard_topology.
Apply xm (Rlt b 0) to the current goal.
Assume Hlt0: Rlt b 0.
Set c to be the term div_SNo b (add_SNo 1 b).
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_lower R b) = open_ray_lower R c.
rewrite the current goal using (bounded_transform_phi_preimage_open_ray_lower_neg_case_eq b HbR Hlt0 Hm1ltb) (from left to right).
Use reflexivity.
rewrite the current goal using HpreEq (from left to right).
We prove the intermediate claim HcR: c ∈ R.
An exact proof term for the current goal is (real_div_SNo b HbR (add_SNo 1 b) (real_add_SNo 1 real_1 b HbR)).
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 Hnlt0: ¬ (Rlt b 0).
We prove the intermediate claim Hb0le: Rle 0 b.
An exact proof term for the current goal is (RleI 0 b real_0 HbR Hnlt0).
Apply xm (b = 0) to the current goal.
Assume Hb0: b = 0.
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_lower R b) = open_ray_lower R 0.
rewrite the current goal using Hb0 (from left to right).
An exact proof term for the current goal is bounded_transform_phi_preimage_open_ray_lower_zero_eq.
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 0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_lower_in_open_rays_subbasis R 0 real_0).
An exact proof term for the current goal is (open_rays_subbasis_sub_order_topology_R (open_ray_lower R 0) HsRay).
Assume HbNeq0: ¬ (b = 0).
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 H0ltb: Rlt 0 b.
Apply (SNoLt_trichotomy_or_impred b 0 HbS SNo_0 (Rlt 0 b)) to the current goal.
Assume Hlt: b < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt0 (RltI b 0 HbR real_0 Hlt)).
Assume Heq: b = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HbNeq0 Heq).
Assume Hgt: 0 < b.
An exact proof term for the current goal is (RltI 0 b real_0 HbR Hgt).
Set c to be the term div_SNo b (add_SNo 1 (minus_SNo b)).
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_lower R b) = open_ray_lower R c.
rewrite the current goal using (bounded_transform_phi_preimage_open_ray_lower_pos_case_eq b HbR H0ltb Hblt1) (from left to right).
Use reflexivity.
rewrite the current goal using HpreEq (from left to right).
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_div_SNo b HbR (add_SNo 1 (minus_SNo b)) (real_add_SNo 1 real_1 (minus_SNo b) HmbR)).
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).
∎