proposition: Lemma partition0 (T : finType) (P : {set {set T}}) (D : {set T}) : partition P D -> set0 \in P = false.
proof: Proof. case/and3P => _ _. by apply: contraNF. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)