proposition: Lemma first_proj_fi g: sgraph g -> (injection (first_proj g) <-> functional_graph g).
proof: Proof. move=> gg. have fpf: (function (first_proj g)) by apply: first_proj_f. have Ht: source (first_proj g) = g by rewrite/first_proj; aw. rewrite /injection Ht. split. move=> [_ hyp] a b b'; rewrite /related => i1 i2. suff: (J a b = J a b') by apply: pr2_def. by apply: hyp=>//; do 2 rewrite first_proj_V=>//; aw. move => H;split=>//; move=>x y xg yg/=; do 2 rewrite first_proj_V=>//. by move/functionalP : (conj gg H) => [_]; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)