Let t be given.
Assume HtR: t ∈ R.
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 HmtR: minus_SNo t ∈ R.
An exact proof term for the current goal is (real_minus_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 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 (λu : set ⇒ div_SNo u (add_SNo 1 (abs_SNo u))).
Use reflexivity.
We prove the intermediate claim Hphi_t: 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 (λu : set ⇒ div_SNo u (add_SNo 1 (abs_SNo u))) t HtR) (from left to right).
Use reflexivity.
We prove the intermediate claim Hphi_mt: apply_fun bounded_transform_phi (minus_SNo t) = div_SNo (minus_SNo t) (add_SNo 1 (abs_SNo (minus_SNo t))).
rewrite the current goal using HphiDef (from left to right).
rewrite the current goal using (apply_fun_graph R (λu : set ⇒ div_SNo u (add_SNo 1 (abs_SNo u))) (minus_SNo t) HmtR) (from left to right).
Use reflexivity.
rewrite the current goal using Hphi_mt (from left to right).
rewrite the current goal using (abs_SNo_minus t HtS) (from left to right).
rewrite the current goal using Hphi_t (from left to right).
An exact proof term for the current goal is (div_SNo_minus_num t den HtS HdenS Hden0).
∎