proposition: Fact setpart1_bottom P : (setpart1 S <= P)%O.
proof: Proof. apply/is_finer_pblockP=> x xinS. rewrite pblock_setpart1 //; apply/subsetP=> y. by rewrite inE => /eqP->; rewrite mem_pblock cover_setpart. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition