proposition: Lemma sum_roots : #|A| = \sum_(x in roots e | x \in A) #|connect e x|.
proof: Proof. under [RHS]eq_bigl => ? do rewrite andbC. rewrite (card_partition rpP) (set_partition_big_cond _ rpP) /=. apply: eq_bigr => B /imsetP [x]; rewrite inE => /andP[x_A root_x] ->. rewrite (big_pred1 x) ?cardsE // => y; rewrite !inE. apply/andP/eqP => [[xy root_y]|->//]. by rewrite -(eqP root_y) -(rootP sym_e xy) (eqP root_x). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)