proposition: Theorem compg_inverse: {morph inverse_graph : a b / a \cg b >-> b \cg a}.
proof: Proof. move => r r';set_extens x. move/igraphP => [px] /compg_pP [z pa pb]. by rewrite -px; apply/compg_pP; exists z => //; apply/igraph_pP. move/compg_P => [px [y /igraph_pP pa /igraph_pP pb]]. by rewrite -px; apply/igraph_pP/compg_pP; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)