Let s be given.
Assume HsI: s ∈ open_interval (minus_SNo 1) 1.
We prove the intermediate claim HsR: s ∈ R.
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 HsS: SNo s.
An exact proof term for the current goal is (real_SNo s HsR).
We prove the intermediate claim HmsR: minus_SNo s ∈ R.
An exact proof term for the current goal is (real_minus_SNo s HsR).
We prove the intermediate claim HabLt1: abs_SNo s < 1.
An exact proof term for the current goal is (abs_lt_one_of_open_interval s HsI).
We prove the intermediate claim HabsR: abs_SNo s ∈ R.
An exact proof term for the current goal is (abs_SNo_in_R s HsR).
We prove the intermediate claim HabsS: SNo (abs_SNo s).
An exact proof term for the current goal is (real_SNo (abs_SNo s) HabsR).
Set den to be the term add_SNo 1 (minus_SNo (abs_SNo s)).
We prove the intermediate claim HdenS: SNo den.
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo (abs_SNo s)) SNo_1 (SNo_minus_SNo (abs_SNo s) HabsS)).
We prove the intermediate claim Hneg1LtNegAbs: minus_SNo 1 < minus_SNo (abs_SNo s).
An exact proof term for the current goal is (minus_SNo_Lt_contra (abs_SNo s) 1 HabsS SNo_1 HabLt1).
We prove the intermediate claim HdenPos0: add_SNo 1 (minus_SNo 1) < den.
An exact proof term for the current goal is (add_SNo_Lt2 1 (minus_SNo 1) (minus_SNo (abs_SNo s)) SNo_1 (SNo_minus_SNo 1 SNo_1) (SNo_minus_SNo (abs_SNo s) HabsS) Hneg1LtNegAbs).
We prove the intermediate claim HdenPos: 0 < den.
rewrite the current goal using (add_SNo_minus_SNo_rinv 1 SNo_1) (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 HpsiDef: bounded_transform_psi = graph R (λu : set ⇒ div_SNo u (add_SNo 1 (minus_SNo (abs_SNo u)))).
Use reflexivity.
We prove the intermediate claim Hpsi_s: apply_fun bounded_transform_psi s = div_SNo s den.
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λu : set ⇒ div_SNo u (add_SNo 1 (minus_SNo (abs_SNo u)))) s HsR) (from left to right).
Use reflexivity.
We prove the intermediate claim Hpsi_ms: apply_fun bounded_transform_psi (minus_SNo s) = div_SNo (minus_SNo s) (add_SNo 1 (minus_SNo (abs_SNo (minus_SNo s)))).
rewrite the current goal using HpsiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λu : set ⇒ div_SNo u (add_SNo 1 (minus_SNo (abs_SNo u)))) (minus_SNo s) HmsR) (from left to right).
Use reflexivity.
rewrite the current goal using Hpsi_ms (from left to right).
rewrite the current goal using (abs_SNo_minus s HsS) (from left to right).
rewrite the current goal using Hpsi_s (from left to right).
An exact proof term for the current goal is (div_SNo_minus_num s den HsS HdenS Hden0).
∎