Let A, f, g and a be given.
Assume Ha: a ∈ A.
Assume HfaR: apply_fun f a ∈ R.
Assume HgaR: apply_fun g a ∈ R.
We will prove apply_fun (compose_fun A (pair_map A f (compose_fun A g neg_fun)) add_fun_R) a = add_SNo (apply_fun f a) (minus_SNo (apply_fun g a)).
We prove the intermediate claim HgnegR: apply_fun (compose_fun A g neg_fun) a ∈ R.
rewrite the current goal using (compose_fun_apply A g neg_fun a Ha) (from left to right).
rewrite the current goal using (neg_fun_apply (apply_fun g a) HgaR) (from left to right).
An exact proof term for the current goal is (real_minus_SNo (apply_fun g a) HgaR).
rewrite the current goal using (add_of_pair_map_apply A f (compose_fun A g neg_fun) a Ha HfaR HgnegR) (from left to right).
rewrite the current goal using (compose_fun_apply A g neg_fun a Ha) (from left to right) at position 1.
rewrite the current goal using (neg_fun_apply (apply_fun g a) HgaR) (from left to right) at position 1.
Use reflexivity.
∎