Let t be given.
Assume HtR: t ∈ R.
We will prove apply_fun bounded_transform_phi t ∈ R.
We prove the intermediate claim Hdef: bounded_transform_phi = graph R (λt0 : set ⇒ div_SNo t0 (add_SNo 1 (abs_SNo t0))).
Use reflexivity.
rewrite the current goal using Hdef (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).
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 HdenR: add_SNo 1 (abs_SNo t) ∈ R.
An exact proof term for the current goal is (real_add_SNo 1 real_1 (abs_SNo t) HabsR).
An exact proof term for the current goal is (real_div_SNo t HtR (add_SNo 1 (abs_SNo t)) HdenR).
∎