proposition: Lemma n_comp0 (T : finType) (e : rel T) (a : {pred T}) : a =i pred0 -> n_comp e a = 0.
proof: Proof. by move=> a0; rewrite (eq_n_comp_r a0); apply: eq_card0 => x; rewrite !inE andbF. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)