proposition: Lemma sumz_connect (I : finType) (e : rel I) (F : I -> int) : connect_sym e -> \sum_(x in roots e) \sum_(y in connect e x) F y = \sum_y F y.
proof: Proof. move=> sym_e. rewrite [RHS](partition_big (root e) (roots e)) => /= [|y _]; last first. exact: roots_root. apply: eq_bigr => x /eqP-Dx; apply: eq_bigl => y. by apply/rootP/eqP; rewrite ?Dx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)