proposition: Lemma eqv_test_equiv: Equivalence eqv_test.
proof: Proof. split => [x|x y|x y z]; rewrite /eqv_test /=. reflexivity. by symmetry. by transitivity (elem_of y). Qed.
imports: HB(structures) Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries setoid_bigop structures)