Apply set_ext to the current goal.
Let t be given.
Assume HtPre: t ∈ preimage_of R bounded_transform_phi (open_ray_lower R 0).
We will prove t ∈ open_ray_lower 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_lower 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_lower R 0.
An exact proof term for the current goal is (SepE2 R (λx : set ⇒ apply_fun bounded_transform_phi x ∈ open_ray_lower R 0) t HtPre).
We prove the intermediate claim Hrel: order_rel R (apply_fun bounded_transform_phi t) 0.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 0) (apply_fun bounded_transform_phi t) HfRay).
We prove the intermediate claim Hltf0: Rlt (apply_fun bounded_transform_phi t) 0.
An exact proof term for the current goal is (order_rel_R_implies_Rlt (apply_fun bounded_transform_phi t) 0 Hrel).
We prove the intermediate claim HfLtS: apply_fun bounded_transform_phi t < 0.
An exact proof term for the current goal is (RltE_lt (apply_fun bounded_transform_phi t) 0 Hltf0).
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 HdivLt: div_SNo t den < 0.
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 HtLt0den: t < mul_SNo 0 den.
An exact proof term for the current goal is (div_SNo_pos_LtL' t den 0 HtS HdenS SNo_0 HdenPos HdivLt).
We prove the intermediate claim HtNegS: t < 0.
rewrite the current goal using (mul_SNo_zeroL den HdenS) (from right to left).
An exact proof term for the current goal is HtLt0den.
We prove the intermediate claim HtNeg: Rlt t 0.
An exact proof term for the current goal is (RltI t 0 HtR real_0 HtNegS).
We prove the intermediate claim HrelT: order_rel R t 0.
An exact proof term for the current goal is (Rlt_implies_order_rel_R t 0 HtNeg).
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 0) t HtR HrelT).
Let t be given.
Assume HtRay: t ∈ open_ray_lower R 0.
We will prove t ∈ preimage_of R bounded_transform_phi (open_ray_lower 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 x0 0) 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 t 0.
An exact proof term for the current goal is (SepE2 R (λx0 : set ⇒ order_rel R x0 0) t HtRay).
We prove the intermediate claim Hlt0t: Rlt t 0.
An exact proof term for the current goal is (order_rel_R_implies_Rlt t 0 HrelT).
We prove the intermediate claim HtNegS: t < 0.
An exact proof term for the current goal is (RltE_lt t 0 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 HdivNeg: div_SNo t den < 0.
An exact proof term for the current goal is (div_SNo_neg_pos t den HtS HdenS HtNegS 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 HfNegS: apply_fun bounded_transform_phi t < 0.
rewrite the current goal using HfEq (from left to right).
An exact proof term for the current goal is HdivNeg.
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 Hltf0: Rlt (apply_fun bounded_transform_phi t) 0.
An exact proof term for the current goal is (RltI (apply_fun bounded_transform_phi t) 0 HfR real_0 HfNegS).
We prove the intermediate claim HrelF: order_rel R (apply_fun bounded_transform_phi t) 0.
An exact proof term for the current goal is (Rlt_implies_order_rel_R (apply_fun bounded_transform_phi t) 0 Hltf0).
We prove the intermediate claim HfRay: apply_fun bounded_transform_phi t ∈ open_ray_lower R 0.
An exact proof term for the current goal is (SepI R (λx0 : set ⇒ order_rel R x0 0) (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_lower R 0) t HtR HfRay).
∎