fact: Definition is_finer_pblockP P Q : reflect (forall x, x \in S -> pblock P x \subset pblock Q x) (P <= Q)%O := is_finer_pblockP P Q.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition