proposition: Lemma partition0 P D : partition P D -> set0 \in P = false.
proof: Proof. case/and3P => _ _. by apply: contraNF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)