proposition: Lemma n_comp_partition : n_comp e A = #|equivalence_partition (connect e) A|.
proof: Proof. rewrite -root_partitionE. rewrite card_in_imset; first by apply: eq_card => z; rewrite !inE andbC. move => x y /set_inP [x_A root_x] /set_inP [y_A root_y] /setP /(_ y). rewrite !inE connect0 -{2}[x](eqP root_x) -{2}[y](eqP root_y) => xy. exact/rootP. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)