Let t be given.
Assume HtR: t ∈ R.
Assume Hflt0: Rlt (apply_fun bounded_transform_phi t) 0.
We will prove Rlt t 0.
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 HfLt0S: 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 Hflt0).
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 HdivLt0: div_SNo t den < 0.
rewrite the current goal using HfEq (from right to left).
An exact proof term for the current goal is HfLt0S.
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 HdivLt0).
We prove the intermediate claim HtLt0S: t < 0.
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 HtLt0den.
An exact proof term for the current goal is (RltI t 0 HtR real_0 HtLt0S).
∎