proposition: Lemma n_compD (T : finType) (a b : {pred T}) e : n_comp e a = n_comp e [predI a & b] + n_comp e [predD a & b].
proof: Proof. rewrite -[LHS](cardID b). by congr (_ + _); apply: eq_card => x; rewrite !inE; case: (roots _ _). Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)