proposition: Lemma sum_rootsT (T : finType) (e : rel T) : connect_sym e -> #|T| = \sum_(x in roots e) #|connect e x|.
proof: Proof. move=> sym_e; rewrite -cardsT (sum_roots sym_e); last exact: closedT. by under eq_bigl => ? do rewrite !inE andbT. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)