Let t be given.
Assume HtR: t ∈ R.
We will prove Rlt (minus_SNo 1) (apply_fun bounded_transform_phi t) ∧ Rlt (apply_fun bounded_transform_phi t) 1.
Set f to be the term apply_fun bounded_transform_phi t.
We prove the intermediate claim HfR: f ∈ R.
An exact proof term for the current goal is (bounded_transform_phi_value_in_R t HtR).
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 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 HdenR: den ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (abs_SNo t) HabsR).
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: f = 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 HtLeAbs: t ≤ abs_SNo t.
An exact proof term for the current goal is (abs_SNo_upper_bound t HtS).
We prove the intermediate claim HabsLtDen_raw: add_SNo (abs_SNo t) 0 < add_SNo (abs_SNo t) 1.
An exact proof term for the current goal is (add_SNo_Lt2 (abs_SNo t) 0 1 HabsS SNo_0 SNo_1 SNoLt_0_1).
We prove the intermediate claim HabsLtAbs1: abs_SNo t < add_SNo (abs_SNo t) 1.
rewrite the current goal using (add_SNo_0R (abs_SNo t) HabsS) (from right to left) at position 1.
An exact proof term for the current goal is HabsLtDen_raw.
We prove the intermediate claim Habs1EqDen: add_SNo (abs_SNo t) 1 = den.
An exact proof term for the current goal is (add_SNo_com (abs_SNo t) 1 HabsS SNo_1).
We prove the intermediate claim HabsLtDen: abs_SNo t < den.
rewrite the current goal using Habs1EqDen (from right to left).
An exact proof term for the current goal is HabsLtAbs1.
We prove the intermediate claim HabS: SNo (abs_SNo t).
An exact proof term for the current goal is HabsS.
We prove the intermediate claim HtLtDen: t < den.
An exact proof term for the current goal is (SNoLeLt_tra t (abs_SNo t) den HtS HabS HdenS HtLeAbs HabsLtDen).
We prove the intermediate claim HnegDenLtNegAbs: minus_SNo den < minus_SNo (abs_SNo t).
An exact proof term for the current goal is (minus_SNo_Lt_contra (abs_SNo t) den HabsS HdenS HabsLtDen).
We prove the intermediate claim HnegAbsLeT: minus_SNo (abs_SNo t) ≤ t.
An exact proof term for the current goal is (abs_SNo_lower_bound t HtS).
We prove the intermediate claim HnegDenLtT: minus_SNo den < t.
We prove the intermediate claim HmdenS: SNo (minus_SNo den).
An exact proof term for the current goal is (SNo_minus_SNo den HdenS).
We prove the intermediate claim HmabsS: SNo (minus_SNo (abs_SNo t)).
An exact proof term for the current goal is (SNo_minus_SNo (abs_SNo t) HabsS).
An exact proof term for the current goal is (SNoLtLe_tra (minus_SNo den) (minus_SNo (abs_SNo t)) t HmdenS HmabsS HtS HnegDenLtNegAbs HnegAbsLeT).
Apply andI to the current goal.
We prove the intermediate claim Hm1S: SNo (minus_SNo 1).
An exact proof term for the current goal is (SNo_minus_SNo 1 SNo_1).
We prove the intermediate claim Hm1denLt: mul_SNo (minus_SNo 1) den < t.
We prove the intermediate claim HmdenEq: mul_SNo (minus_SNo 1) den = minus_SNo den.
rewrite the current goal using (mul_SNo_minus_distrL 1 den SNo_1 HdenS) (from left to right).
rewrite the current goal using (mul_SNo_oneL den HdenS) (from left to right).
Use reflexivity.
rewrite the current goal using HmdenEq (from left to right).
An exact proof term for the current goal is HnegDenLtT.
We prove the intermediate claim Hm1LtDiv: minus_SNo 1 < div_SNo t den.
An exact proof term for the current goal is (div_SNo_pos_LtR t den (minus_SNo 1) HtS HdenS Hm1S HdenPos Hm1denLt).
We prove the intermediate claim Hm1R: minus_SNo 1 ∈ R.
An exact proof term for the current goal is (real_minus_SNo 1 real_1).
We prove the intermediate claim HdivR: div_SNo t den ∈ R.
An exact proof term for the current goal is (real_div_SNo t HtR den HdenR).
We prove the intermediate claim Hm1Ltf: minus_SNo 1 < f.
rewrite the current goal using HfEq (from left to right).
An exact proof term for the current goal is Hm1LtDiv.
An exact proof term for the current goal is (RltI (minus_SNo 1) f Hm1R HfR Hm1Ltf).
We prove the intermediate claim H1S: SNo 1.
An exact proof term for the current goal is SNo_1.
We prove the intermediate claim HtLt1den: t < mul_SNo 1 den.
rewrite the current goal using (mul_SNo_oneL den HdenS) (from left to right).
An exact proof term for the current goal is HtLtDen.
We prove the intermediate claim HdivLt1: div_SNo t den < 1.
An exact proof term for the current goal is (div_SNo_pos_LtL t den 1 HtS HdenS H1S HdenPos HtLt1den).
We prove the intermediate claim Hflt1: f < 1.
rewrite the current goal using HfEq (from left to right) at position 1.
An exact proof term for the current goal is HdivLt1.
An exact proof term for the current goal is (RltI f 1 HfR real_1 Hflt1).
∎