proposition: Lemma igraph_involutive : {when sgraph, involutive inverse_graph}.
proof: Proof. move=> f gr; set_extens x;first by case/igraphP => px /igraph_pP; rewrite px. move => xf; have px:= (gr _ xf). by rewrite -px;apply/igraph_pP /igraph_pP; rewrite px. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)