proposition: Lemma fgraph_to_fun_fs f: fgraph f -> surjection (fgraph_to_fun f).
proof: Proof. move => fgf. have ff: function (fgraph_to_fun f) by apply: function_pr. apply:(surjective_pr5 ff); rewrite /fgraph_to_fun;aw. by move => y /(range_gP fgf) [x xdf ->]; ex_tac; apply:fdomain_pr1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)