proposition: Lemma partition_set0 P : partition P set0 = (P == set0).
proof: Proof. apply/and3P/eqP => [[/bigcup0P covP _ ]|->]; last first. by rewrite /partition inE /trivIset/cover !big_set0 cards0 !eqxx. by apply: contraNeq => /set0Pn[B BP]; rewrite -(covP B BP). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)