proposition: Lemma eao_P r x y: related (equivalence_associated_o r) x y <-> symmetrize (gle r) x y.
proof: Proof. split; first by move /setI2_P =>[pa] /igraph_pP pb; split. by move => [pa pb]; apply:setI2_i => //; apply /igraph_pP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)