Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R bounded_transform_phi (open_ray_upper R 0).
We will prove t ∈ open_ray_upper R 0.
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx : set ⇒ apply_fun bounded_transform_phi x ∈ open_ray_upper R 0) t HtPre).
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 HfRay: apply_fun bounded_transform_phi t ∈ open_ray_upper R 0.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun bounded_transform_phi x ∈ open_ray_upper R 0) t HtPre).
We prove the intermediate claim Hrel: order_rel R 0 (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R 0 x0) (apply_fun bounded_transform_phi t) HfRay).
We prove the intermediate claim Hlt0f: Rlt 0 (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (order_rel_R_implies_Rlt 0 (apply_fun bounded_transform_phi t) Hrel).
We prove the intermediate claim HfLtS: 0 < apply_fun bounded_transform_phi t.
An exact proof term for the current goal is (RltE_lt 0 (apply_fun bounded_transform_phi t) Hlt0f).
We prove the intermediate claim HabsR: abs_SNo t ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R t HtR).
We prove the intermediate claim HabsS: SNo (abs_SNo t).
An exact proof term for the current goal is (real_SNo (abs_SNo t) HabsR).
Set den to be the term add_SNo 1 (abs_SNo t).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (SNo_add_SNo 1 (abs_SNo t) SNo_1 HabsS).
We prove the intermediate claim H0le_abs: 0 ≤ abs_SNo t.
An exact proof term for the current goal is (abs_SNo_nonneg t 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 (abs_SNo t) SNo_0 SNo_0 SNo_1 HabsS SNoLt_0_1 H0le_abs).
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 HfEq: 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).
Use reflexivity.
We prove the intermediate claim HdivPos: 0 < div_SNo t den.
rewrite the current goal using HfEq (from right to left).
An exact proof term for the current goal is HfLtS.
We prove the intermediate claim H0denLt: mul_SNo 0 den < t.
An exact proof term for the current goal is (div_SNo_pos_LtR' t den 0 HtS HdenS SNo_0 HdenPos HdivPos).
We prove the intermediate claim HtPosS: 0 < t.
rewrite the current goal using (mul_SNo_zeroL den HdenS) (from right to left) at position 1.
An exact proof term for the current goal is H0denLt.
We prove the intermediate claim HtPos: Rlt 0 t.
An exact proof term for the current goal is (RltI 0 t real_0 HtR HtPosS).
We prove the intermediate claim HrelT: order_rel R 0 t.
An exact proof term for the current goal is (Rlt_implies_order_rel_R 0 t HtPos).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R 0 x0) t HtR HrelT).
Let t be given.
Assume HtRay: t ∈ open_ray_upper R 0.
We will prove t ∈ preimage_of R bounded_transform_phi (open_ray_upper R 0).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (SepE1 R (λx0 : set ⇒ order_rel R 0 x0) t HtRay).
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 HrelT: order_rel R 0 t.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R 0 x0) t HtRay).
We prove the intermediate claim Hlt0t: Rlt 0 t.
An exact proof term for the current goal is (order_rel_R_implies_Rlt 0 t HrelT).
We prove the intermediate claim HtPosS: 0 < t.
An exact proof term for the current goal is (RltE_lt 0 t Hlt0t).
We prove the intermediate claim HabsR: abs_SNo t ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R t HtR).
We prove the intermediate claim HabsS: SNo (abs_SNo t).
An exact proof term for the current goal is (real_SNo (abs_SNo t) HabsR).
Set den to be the term add_SNo 1 (abs_SNo t).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (SNo_add_SNo 1 (abs_SNo t) SNo_1 HabsS).
We prove the intermediate claim H0le_abs: 0 ≤ abs_SNo t.
An exact proof term for the current goal is (abs_SNo_nonneg t 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 (abs_SNo t) SNo_0 SNo_0 SNo_1 HabsS SNoLt_0_1 H0le_abs).
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 HdivPos: 0 < div_SNo t den.
An exact proof term for the current goal is (div_SNo_pos_pos t den HtS HdenS HtPosS HdenPos).
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 HfEq: 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).
Use reflexivity.
We prove the intermediate claim HfPos: 0 < apply_fun bounded_transform_phi t.
rewrite the current goal using HfEq (from left to right).
An exact proof term for the current goal is HdivPos.
We prove the intermediate claim HfR: 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 Hlt0f: 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 HfR HfPos).
We prove the intermediate claim HrelF: order_rel R 0 (apply_fun bounded_transform_phi t).
An exact proof term for the current goal is (Rlt_implies_order_rel_R 0 (apply_fun bounded_transform_phi t) Hlt0f).
We prove the intermediate claim HfRay: apply_fun bounded_transform_phi t ∈ open_ray_upper R 0.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R 0 x0) (apply_fun bounded_transform_phi t) HfR HrelF).
An exact proof term for the current goal is (SepI R (λx : set ⇒ apply_fun bounded_transform_phi x ∈ open_ray_upper R 0) t HtR HfRay).
∎