proposition: Lemma compose3_relP s r u v: related ((s \cg r) \cg (opp_order s)) u v <-> exists x y, [/\ related s x u, related s y v& related r x y].
proof: Proof. split. by move/compg_pP => [z /igraph_pP pa /compg_pP [y pb pc]]; exists z, y. move=> [x [y [xu yv xy]]]; apply/compg_pP;exists x; first by apply/igraph_pP. by apply/compg_pP; exists y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)