proposition: Lemma connect_symI (T : finType) (e : rel T) : symmetric e -> connect_sym e.
proof: Proof. move => sym_e; suff S x y : connect e x y -> connect e y x. move => x y. apply/idP/idP; exact: S. case/connectP => p; elim: p x y => /= [x y _ -> //|z p IH x y /andP [A B] C]. rewrite sym_e in A; apply: connect_trans (connect1 A); exact: IH. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)