proposition: Lemma setpart_set0_eq_set0 (p : setpart set0) : p = setpart_set0.
proof: Proof. case: p=> p Hp; apply/eqP. by rewrite eqE /= -partition_set0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition