proposition: Lemma eq_connect_sym (T : finType) (e e' : rel T) : e =2 e' -> connect_sym e -> connect_sym e'.
proof: Proof. by move=> eq_e sym_e x y; rewrite -!(eq_connect eq_e). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)