Let t be given.
Assume HtR: t ∈ R.
Assume H0ltf: Rlt 0 (apply_fun bounded_transform_phi t).
We will prove Rlt 0 t.
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 H0ltfS: 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) H0ltf).
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 H0ltfS.
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.
An exact proof term for the current goal is (RltI 0 t real_0 HtR HtPosS).
∎