proposition: Lemma selfinverse_graph_symmetric r: sgraph r -> (symmetricp r <-> (r = inverse_graph r)).
proof: Proof. move => gr; split => sp; last by move => x y Jr; rewrite sp; apply/igraph_pP. set_extens t => tr. move: (gr _ tr) => aux. by rewrite - aux; apply/igraph_pP; apply: sp; hnf; rewrite aux. by move /igraphP: tr => [pt pa]; rewrite -pt; apply: sp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)