proposition: Lemma inv_graph_canon_fb g: sgraph g -> bijection ( Lf (fun x=> J (Q x) (P x)) g (inverse_graph g)).
proof: Proof. move => gg; apply: lf_bijective. + by move=> c cg /=; apply/igraph_pP; rewrite /related (gg _ cg). + move=> u v ug vg peq; apply: pair_exten; try apply: gg=>//. by apply: (pr2_def peq). by apply: (pr1_def peq). + by move=> y /igraphP [py pg]; ex_tac;aw; rewrite py. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)