proposition: Lemma setpart_non0 P : set0 \notin P.
proof: Proof. by case: P => P /= /and3P[]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition