An exact proof term for the current goal is (apply_fun_graph R (λx0 : set ⇒ (x0,div_SNo (add_SNo c (minus_SNo (mul_SNo a x0))) b)) x HxR).