proposition: Lemma sym_connect_sym e : symmetric e -> connect_sym e.
proof: Proof. by move=> sym_e x y; rewrite (eq_connect sym_e) connect_rev. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)