Let t be given.
Assume HtR: t ∈ R.
We will prove apply_fun bounded_transform_psi (apply_fun bounded_transform_phi t) = t.
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
Set den to be the term add_SNo 1 (abs_SNo t).
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).
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 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.
Set s to be the term apply_fun bounded_transform_phi t.
We prove the intermediate claim HsDef0: s = apply_fun bounded_transform_phi t.
Use reflexivity.
rewrite the current goal using HsDef0 (from right to left) at position 1.
We prove the intermediate claim HsDef: s = 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 HsR: s ∈ R.
An exact proof term for the current goal is (bounded_transform_phi_value_in_R t HtR).
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 HabsSDef: abs_SNo s = div_SNo (abs_SNo t) den.
rewrite the current goal using HsDef (from left to right).
An exact proof term for the current goal is (abs_div_SNo_pos t den HtS HdenS HdenPos).
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.
We prove the intermediate claim HpsiEq: apply_fun bounded_transform_psi s = div_SNo s (add_SNo 1 (minus_SNo (abs_SNo s))).
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).
Use reflexivity.
rewrite the current goal using HpsiEq (from left to right) at position 1.
rewrite the current goal using HsDef (from left to right) at position 1.
rewrite the current goal using HabsSDef (from left to right).
Set denom2 to be the term add_SNo 1 (minus_SNo (div_SNo (abs_SNo t) den)).
We prove the intermediate claim Hdenom2Def: denom2 = add_SNo 1 (minus_SNo (div_SNo (abs_SNo t) den)).
Use reflexivity.
We prove the intermediate claim HdivAbsS: SNo (div_SNo (abs_SNo t) den).
An exact proof term for the current goal is (SNo_div_SNo (abs_SNo t) den HabsS HdenS).
We prove the intermediate claim HminS: SNo (minus_SNo (div_SNo (abs_SNo t) den)).
An exact proof term for the current goal is (SNo_minus_SNo (div_SNo (abs_SNo t) den) HdivAbsS).
We prove the intermediate claim Hdenom2S: SNo denom2.
rewrite the current goal using Hdenom2Def (from left to right).
An exact proof term for the current goal is (SNo_add_SNo 1 (minus_SNo (div_SNo (abs_SNo t) den)) SNo_1 HminS).
rewrite the current goal using Hdenom2Def (from right to left) at position 1.
rewrite the current goal using (div_div_SNo t den denom2 HtS HdenS Hdenom2S) (from left to right).
We prove the intermediate claim HdenMul: mul_SNo den denom2 = 1.
rewrite the current goal using Hdenom2Def (from left to right).
rewrite the current goal using (mul_SNo_distrL den 1 (minus_SNo (div_SNo (abs_SNo t) den)) HdenS SNo_1 HminS) (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 (abs_SNo t) den) HdenS HdivAbsS) (from left to right).
rewrite the current goal using (mul_div_SNo_invR (abs_SNo t) den HabsS HdenS Hden0) (from left to right).
We prove the intermediate claim HdenDef: den = add_SNo 1 (abs_SNo t).
Use reflexivity.
rewrite the current goal using HdenDef (from left to right).
rewrite the current goal using (add_SNo_assoc 1 (abs_SNo t) (minus_SNo (abs_SNo t)) SNo_1 HabsS (SNo_minus_SNo (abs_SNo t) HabsS)) (from right to left) at position 1.
rewrite the current goal using (add_SNo_minus_SNo_rinv (abs_SNo t) HabsS) (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 HdenMul (from left to right).
We prove the intermediate claim Hdiv1: div_SNo t 1 = t.
Apply (mul_div_SNo_nonzero_eq t 1 t HtS SNo_1 HtS neq_1_0) to the current goal.
rewrite the current goal using (mul_SNo_oneL t HtS) (from left to right).
Use reflexivity.
rewrite the current goal using Hdiv1 (from left to right).
Use reflexivity.
∎