proposition: Lemma connect_equivalence : equivalence_rel (connect e).
proof: Proof. by rewrite equivalence_relP; split; by [apply: connect0|apply: same_connect]. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)