Let t be given.

Assume HtR: t ∈ R.

We will prove apply_fun neg_fun t ∈ R.

We prove the intermediate claim Hdef: neg_fun = graph R (λt0 : set ⇒ 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 ⇒ minus_SNo t0) t HtR) (from left to right).

An exact proof term for the current goal is (real_minus_SNo t HtR).

∎