proposition: Lemma partition_ni_set0 (T:finType) (P: {set {set T}}) E i: partition P E -> i \in P -> i != set0.
proof: Proof. by move /and3P => [_ _ /negP n0P]; apply:contraTneq => ->; apply /negP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)