We will prove apply_fun one_minus_fun 0 = 1.
We prove the intermediate claim H0R: 0 ∈ R.
An exact proof term for the current goal is real_0.
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)) 0 H0R) (from left to right).
rewrite the current goal using (minus_SNo_0) (from left to right).
rewrite the current goal using (add_SNo_0R 1 SNo_1) (from left to right).
Use reflexivity.
∎