Let t be given.
Assume HtIpos: t ∈ open_ray_upper R 0.
Set Ipos to be the term open_ray_upper R 0.
Set r to be the term compose_fun Ipos (compose_fun R bounded_transform_phi one_minus_fun) bounded_transform_psi.
Set h to be the term compose_fun R bounded_transform_phi one_minus_fun.
We prove the intermediate claim HIposSubR: Ipos ⊆ R.
Let x be given.
Assume HxI: x ∈ Ipos.
An exact proof term for the current goal is (SepE1 R (λy : set ⇒ order_rel R 0 y) x HxI).
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 (λy : set ⇒ order_rel R 0 y) 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 HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim H0lttS: 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 H0lttS).
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 Hden0: den ≠ 0.
An exact proof term for the current goal is (SNo_pos_ne0 den HdenS 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 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 HhEq: apply_fun h t = div_SNo 1 den.
We prove the intermediate claim Hht: 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 Hht (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 (bounded_transform_phi_value_in_R t HtR).
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 HaEq: a = div_SNo t den.
rewrite the current goal using HphiEq (from left to right).
Use reflexivity.
rewrite the current goal using HaEq (from left to right).
We prove the intermediate claim HoneDef: one_minus_fun = graph R (λu : set ⇒ add_SNo 1 (minus_SNo u)).
Use reflexivity.
We prove the intermediate claim HoneApp: apply_fun one_minus_fun (div_SNo t den) = add_SNo 1 (minus_SNo (div_SNo t den)).
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)) (div_SNo t den) (real_div_SNo t HtR den (real_add_SNo 1 real_1 t HtR))) (from left to right).
Use reflexivity.
rewrite the current goal using HoneApp (from left to right).
Set y to be the term add_SNo 1 (minus_SNo (div_SNo t den)).
We prove the intermediate claim HyS: SNo y.
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo (div_SNo t den)) SNo_1 (SNo_minus_SNo (div_SNo t den) (SNo_div_SNo t den HtS HdenS))).
We prove the intermediate claim Hden_y: mul_SNo den y = 1.
rewrite the current goal using (mul_SNo_distrL den 1 (minus_SNo (div_SNo t den)) HdenS SNo_1 (SNo_minus_SNo (div_SNo t den) (SNo_div_SNo t den HtS HdenS))) (from left to right).
rewrite the current goal using (mul_SNo_oneR den HdenS) (from left to right).
rewrite the current goal using (mul_SNo_minus_distrR den (div_SNo t den) HdenS (SNo_div_SNo t den HtS HdenS)) (from left to right).
rewrite the current goal using (mul_div_SNo_invR t den HtS HdenS Hden0) (from left to right).
We prove the intermediate claim HdenDef: den = add_SNo 1 t.
Use reflexivity.
rewrite the current goal using HdenDef (from left to right).
rewrite the current goal using (add_SNo_assoc 1 t (minus_SNo t) SNo_1 HtS (SNo_minus_SNo t HtS)) (from right to left) at position 1.
rewrite the current goal using (add_SNo_minus_SNo_rinv t HtS) (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from left to right).
Use reflexivity.
We prove the intermediate claim Hden_div: mul_SNo den (div_SNo 1 den) = 1.
An exact proof term for the current goal is (mul_div_SNo_invR 1 den SNo_1 HdenS Hden0).
We prove the intermediate claim HyEq: y = div_SNo 1 den.
Apply (mul_SNo_nonzero_cancel den y (div_SNo 1 den) HdenS Hden0 HyS (SNo_div_SNo 1 den SNo_1 HdenS)) to the current goal.
rewrite the current goal using Hden_y (from left to right).
rewrite the current goal using Hden_div (from left to right).
Use reflexivity.
An exact proof term for the current goal is HyEq.
We prove the intermediate claim HrEq: apply_fun r t = recip_SNo_pos t.
We prove the intermediate claim Hrt: apply_fun r t = apply_fun bounded_transform_psi (apply_fun h t).
rewrite the current goal using (compose_fun_apply Ipos h bounded_transform_psi t HtIpos) (from left to right).
Use reflexivity.
rewrite the current goal using Hrt (from left to right).
rewrite the current goal using HhEq (from left to right).
Set s to be the term div_SNo 1 den.
We prove the intermediate claim HsDef: s = div_SNo 1 den.
Use reflexivity.
We prove the intermediate claim HsR: s ∈ R.
An exact proof term for the current goal is (real_div_SNo 1 real_1 den (real_add_SNo 1 real_1 t HtR)).
We prove the intermediate claim HpsiDef: bounded_transform_psi = graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))).
Use reflexivity.
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λs0 : set ⇒ div_SNo s0 (add_SNo 1 (minus_SNo (abs_SNo s0)))) s HsR) (from left to right).
Set denom2 to be the term add_SNo 1 (minus_SNo (abs_SNo s)).
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 HsposS: 0 < s.
An exact proof term for the current goal is (div_SNo_pos_pos 1 den SNo_1 HdenS SNoLt_0_1 HdenPos).
We prove the intermediate claim H0les: 0 ≤ s.
An exact proof term for the current goal is (SNoLtLe 0 s HsposS).
We prove the intermediate claim HabsS: abs_SNo s = s.
An exact proof term for the current goal is (nonneg_abs_SNo s H0les).
rewrite the current goal using HabsS (from left to right).
Set denom3 to be the term add_SNo 1 (minus_SNo s).
We prove the intermediate claim Hdenom3S: SNo denom3.
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo s) SNo_1 (SNo_minus_SNo s HsS)).
rewrite the current goal using HsDef (from left to right).
rewrite the current goal using (div_div_SNo 1 den denom3 SNo_1 HdenS Hdenom3S) (from left to right).
We prove the intermediate claim HdenMul: mul_SNo den denom3 = t.
rewrite the current goal using (mul_SNo_distrL den 1 (minus_SNo s) HdenS SNo_1 (SNo_minus_SNo s HsS)) (from left to right).
rewrite the current goal using (mul_SNo_oneR den HdenS) (from left to right).
rewrite the current goal using (mul_SNo_minus_distrR den s HdenS HsS) (from left to right).
rewrite the current goal using HsDef (from left to right).
rewrite the current goal using (mul_div_SNo_invR 1 den SNo_1 HdenS Hden0) (from left to right).
We prove the intermediate claim HdenDef: den = add_SNo 1 t.
Use reflexivity.
rewrite the current goal using HdenDef (from left to right).
rewrite the current goal using (add_SNo_com 1 t SNo_1 HtS) (from left to right) at position 1.
rewrite the current goal using (add_SNo_minus_R2 t 1 HtS SNo_1) (from left to right).
Use reflexivity.
rewrite the current goal using HdenMul (from left to right).
We prove the intermediate claim HdivDef: div_SNo 1 t = mul_SNo 1 (recip_SNo t).
Use reflexivity.
We prove the intermediate claim Hposcase: recip_SNo t = recip_SNo_pos t.
An exact proof term for the current goal is (recip_SNo_poscase t H0lttS).
rewrite the current goal using HdivDef (from left to right).
rewrite the current goal using Hposcase (from left to right).
rewrite the current goal using (mul_SNo_oneL (recip_SNo_pos t) (SNo_recip_SNo_pos t HtS H0lttS)) (from left to right).
Use reflexivity.
An exact proof term for the current goal is HrEq.
∎