We will prove continuous_map (open_ray_upper R 0) (subspace_topology R R_standard_topology (open_ray_upper R 0)) R R_standard_topology (compose_fun (open_ray_upper R 0) (compose_fun R bounded_transform_phi one_minus_fun) bounded_transform_psi).
Set Ipos to be the term open_ray_upper R 0.
Set Tpos to be the term subspace_topology R R_standard_topology Ipos.
Set I to be the term open_interval (minus_SNo 1) 1.
Set Ti to be the term subspace_topology R R_standard_topology I.
Set h to be the term compose_fun R bounded_transform_phi one_minus_fun.
We prove the intermediate claim HIposSubR: Ipos ⊆ R.
Let t be given.
Assume HtIpos: t ∈ Ipos.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ order_rel R 0 x) t HtIpos).
We prove the intermediate claim HI_sub_R: I ⊆ R.
Let s be given.
Assume HsI: s ∈ I.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) s HsI).
We prove the intermediate claim HTpos: topology_on Ipos Tpos.
An exact proof term for the current goal is (subspace_topology_is_topology R R_standard_topology Ipos R_standard_topology_is_topology HIposSubR).
We prove the intermediate claim HTi: topology_on I Ti.
An exact proof term for the current goal is (subspace_topology_is_topology R R_standard_topology I R_standard_topology_is_topology HI_sub_R).
We prove the intermediate claim Hh_cont_R: continuous_map R R_standard_topology R R_standard_topology h.
An exact proof term for the current goal is (composition_continuous R R_standard_topology R R_standard_topology R R_standard_topology bounded_transform_phi one_minus_fun bounded_transform_phi_continuous one_minus_fun_continuous).
We prove the intermediate claim Hh_cont_pos_R: continuous_map Ipos Tpos R R_standard_topology h.
An exact proof term for the current goal is (continuous_on_subspace_rule R R_standard_topology R R_standard_topology h Ipos R_standard_topology_is_topology R_standard_topology_is_topology HIposSubR Hh_cont_R).
We prove the intermediate claim Hh_img_I: ∀t : set, t ∈ Ipos → apply_fun h t ∈ I.
Let t be given.
Assume HtIpos: t ∈ Ipos.
We will prove apply_fun h t ∈ I.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (HIposSubR t HtIpos).
We prove the intermediate claim HtRel: order_rel R 0 t.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ order_rel R 0 x) t HtIpos).
We prove the intermediate claim H0ltT: Rlt 0 t.
An exact proof term for the current goal is (order_rel_R_implies_Rlt 0 t HtRel).
We prove the intermediate claim HphiBnds: Rlt (minus_SNo 1) (apply_fun bounded_transform_phi t) ∧ Rlt (apply_fun bounded_transform_phi t) 1.
An exact proof term for the current goal is (bounded_transform_phi_strict_bounds t HtR).
We prove the intermediate claim HphiLt1: Rlt (apply_fun bounded_transform_phi t) 1.
An exact proof term for the current goal is (andER (Rlt (minus_SNo 1) (apply_fun bounded_transform_phi t)) (Rlt (apply_fun bounded_transform_phi t) 1) HphiBnds).
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 HtPosS: 0 < t.
An exact proof term for the current goal is (RltE_lt 0 t H0ltT).
We prove the intermediate claim H0leT: 0 ≤ t.
An exact proof term for the current goal is (SNoLtLe 0 t HtPosS).
We prove the intermediate claim HabsEq: abs_SNo t = t.
An exact proof term for the current goal is (nonneg_abs_SNo t H0leT).
Set den to be the term add_SNo 1 t.
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (SNo_add_SNo 1 t SNo_1 HtS).
We prove the intermediate claim HdenPos0: add_SNo 0 0 < den.
An exact proof term for the current goal is (add_SNo_Lt3a 0 0 1 t SNo_0 SNo_0 SNo_1 HtS SNoLt_0_1 H0leT).
We prove the intermediate claim HdenPos: 0 < den.
rewrite the current goal using (add_SNo_0L 0 SNo_0) (from right to left) at position 1.
An exact proof term for the current goal is HdenPos0.
We prove the intermediate claim HphiDef: bounded_transform_phi = graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))).
Use reflexivity.
We prove the intermediate claim HphiEq: apply_fun bounded_transform_phi t = div_SNo t den.
rewrite the current goal using HphiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))) t HtR) (from left to right).
rewrite the current goal using HabsEq (from left to right).
Use reflexivity.
We prove the intermediate claim HphiPosS: 0 < apply_fun bounded_transform_phi t.
rewrite the current goal using HphiEq (from left to right).
An exact proof term for the current goal is (div_SNo_pos_pos t den HtS HdenS HtPosS HdenPos).
We prove the intermediate claim HphiR: apply_fun bounded_transform_phi t ∈ R.
An exact proof term for the current goal is (bounded_transform_phi_value_in_R t HtR).
We prove the intermediate claim HphiPos: Rlt 0 (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (RltI 0 (apply_fun bounded_transform_phi t) real_0 HphiR HphiPosS).
We prove the intermediate claim HhEq: apply_fun h t = apply_fun one_minus_fun (apply_fun bounded_transform_phi t).
rewrite the current goal using (compose_fun_apply R bounded_transform_phi one_minus_fun t HtR) (from left to right).
Use reflexivity.
rewrite the current goal using HhEq (from left to right).
Set a to be the term apply_fun bounded_transform_phi t.
We prove the intermediate claim HaR: a ∈ R.
An exact proof term for the current goal is HphiR.
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 HoneApp: apply_fun one_minus_fun a = add_SNo 1 (minus_SNo a).
We prove the intermediate claim HoneDef: one_minus_fun = graph R (λu : set ⇒ add_SNo 1 (minus_SNo u)).
Use reflexivity.
rewrite the current goal using HoneDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λu : set ⇒ add_SNo 1 (minus_SNo u)) a HaR) (from left to right).
Use reflexivity.
rewrite the current goal using HoneApp (from left to right).
Set s to be the term add_SNo 1 (minus_SNo a).
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo a) (real_minus_SNo a HaR)).
We prove the intermediate claim HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsR).
We prove the intermediate claim HaLt1S: a < 1.
An exact proof term for the current goal is (RltE_lt a 1 HphiLt1).
We prove the intermediate claim HsPosS: 0 < s.
We prove the intermediate claim HsumLt: add_SNo 0 a < add_SNo s a.
rewrite the current goal using (add_SNo_0L a HaS) (from left to right).
We prove the intermediate claim HsaEq: add_SNo s a = 1.
We prove the intermediate claim HsDef: s = add_SNo 1 (minus_SNo a).
Use reflexivity.
rewrite the current goal using HsDef (from left to right).
rewrite the current goal using (add_SNo_assoc 1 (minus_SNo a) a SNo_1 (SNo_minus_SNo a HaS) HaS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv a HaS) (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from left to right).
Use reflexivity.
rewrite the current goal using HsaEq (from left to right).
An exact proof term for the current goal is HaLt1S.
An exact proof term for the current goal is (add_SNo_Lt1_cancel 0 a s SNo_0 HaS HsS HsumLt).
We prove the intermediate claim HsPos: Rlt 0 s.
An exact proof term for the current goal is (RltI 0 s real_0 HsR HsPosS).
We prove the intermediate claim Hm10: Rlt (minus_SNo 1) 0.
An exact proof term for the current goal is Rlt_minus1_0.
We prove the intermediate claim Hm1ltS: Rlt (minus_SNo 1) s.
An exact proof term for the current goal is (Rlt_tra (minus_SNo 1) 0 s Hm10 HsPos).
We prove the intermediate claim HmA0S: minus_SNo a < 0.
rewrite the current goal using minus_SNo_0 (from right to left) at position 1.
An exact proof term for the current goal is (minus_SNo_Lt_contra 0 a SNo_0 HaS HphiPosS).
We prove the intermediate claim HsLt1S: s < 1.
We prove the intermediate claim HsDef: s = add_SNo 1 (minus_SNo a).
Use reflexivity.
rewrite the current goal using HsDef (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from right to left) at position 2.
An exact proof term for the current goal is (add_SNo_Lt2 1 (minus_SNo a) 0 SNo_1 (SNo_minus_SNo a HaS) SNo_0 HmA0S).
We prove the intermediate claim HsLt1: Rlt s 1.
An exact proof term for the current goal is (RltI s 1 HsR real_1 HsLt1S).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ Rlt (minus_SNo 1) x0 ∧ Rlt x0 1) s HsR (andI (Rlt (minus_SNo 1) s) (Rlt s 1) Hm1ltS HsLt1)).
We prove the intermediate claim Hh_cont_pos_I: continuous_map Ipos Tpos I Ti h.
An exact proof term for the current goal is (continuous_map_range_restrict Ipos Tpos R R_standard_topology h I Hh_cont_pos_R HI_sub_R Hh_img_I).
We prove the intermediate claim Hpsi_cont: continuous_map I Ti R R_standard_topology bounded_transform_psi.
An exact proof term for the current goal is bounded_transform_psi_continuous_open_interval.
An exact proof term for the current goal is (composition_continuous Ipos Tpos I Ti R R_standard_topology h bounded_transform_psi Hh_cont_pos_I Hpsi_cont).
∎