proposition: Lemma igraph_alt r: sgraph r -> inverse_graph r = fun_image r (fun z => J (Q z) (P z)).
proof: Proof. move=> gr; set_extens t. by move /igraphP => [pt h];apply/funI_P; ex_tac; aw; rewrite pt. by move /funI_P => [c zr ->]; apply/igraph_pP; rewrite (gr _ zr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)