Let t be given.
Assume HtR: t ∈ R.
We will prove apply_fun one_minus_fun t ∈ R.
We prove the intermediate claim Hdef: one_minus_fun = graph R (λt0 : set ⇒ add_SNo 1 (minus_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 ⇒ add_SNo 1 (minus_SNo t0)) t HtR) (from left to right).
An exact proof term for the current goal is (real_add_SNo 1 real_1 (minus_SNo t) (real_minus_SNo t HtR)).
∎