proposition: Lemma partition_set0 (T:finType) (P: {set {set T}}) : partition P set0 = (P == set0).
proof: Proof. apply /idP/eqP. by move /card_partition_aux; rewrite cards0 leqn0 => /eqP /cards0_eq. by move ->; rewrite /partition /trivIset /cover !big_set0 cards0 in_set0 !eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)