Let a be given.
Assume HaR: a ∈ R.
Assume Hm1lta: Rlt (minus_SNo 1) a.
Assume Halt1: Rlt a 1.
We will prove preimage_of R bounded_transform_phi (open_ray_upper R a) ∈ R_standard_topology.
Apply xm (Rlt a 0) to the current goal.
Assume Halt0: Rlt a 0.
Set c to be the term div_SNo a (add_SNo 1 a).
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_upper R a) = open_ray_upper R c.
rewrite the current goal using (bounded_transform_phi_preimage_open_ray_upper_neg_case_eq a HaR Halt0 Hm1lta) (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 a HaR (add_SNo 1 a) (real_add_SNo 1 real_1 a HaR)).
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).
Assume Hnlt0: ¬ (Rlt a 0).
We prove the intermediate claim Ha0le: Rle 0 a.
An exact proof term for the current goal is (RleI 0 a real_0 HaR Hnlt0).
Apply xm (a = 0) to the current goal.
Assume Ha0: a = 0.
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_upper R a) = open_ray_upper R 0.
rewrite the current goal using Ha0 (from left to right).
An exact proof term for the current goal is bounded_transform_phi_preimage_open_ray_upper_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_upper R 0 ∈ open_rays_subbasis R.
An exact proof term for the current goal is (open_ray_upper_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_upper R 0) HsRay).
Assume HaNeq0: ¬ (a = 0).
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 H0lta: Rlt 0 a.
Apply (SNoLt_trichotomy_or_impred a 0 HaS SNo_0 (Rlt 0 a)) to the current goal.
Assume Halt: a < 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (Hnlt0 (RltI a 0 HaR real_0 Halt)).
Assume Heq: a = 0.
Apply FalseE to the current goal.
An exact proof term for the current goal is (HaNeq0 Heq).
Assume Hgt: 0 < a.
An exact proof term for the current goal is (RltI 0 a real_0 HaR Hgt).
Set c to be the term div_SNo a (add_SNo 1 (minus_SNo a)).
We prove the intermediate claim HpreEq: preimage_of R bounded_transform_phi (open_ray_upper R a) = open_ray_upper R c.
rewrite the current goal using (bounded_transform_phi_preimage_open_ray_upper_pos_case_eq a HaR H0lta Halt1) (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 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_div_SNo a HaR (add_SNo 1 (minus_SNo a)) (real_add_SNo 1 real_1 (minus_SNo a) HmaR)).
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).
∎