proposition: Lemma functionalP r: (sgraph r /\ functional_graph r) <-> (fgraph r).
proof: Proof. rewrite /functional_graph /related; split; last first. by move=> fr; split; fprops; move=> x y y'; apply: fgraph_pr. move => [gr eql]; split=>// x y xr yr eqp. move: (xr) (yr); rewrite -(gr _ xr) - (gr _ yr) -eqp => pa pb. by rewrite (eql _ _ _ pa pb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)