proposition: Lemma is_finer_pblockP P Q : reflect (forall x, x \in S -> pblock P x \subset pblock Q x) (is_finer P Q).
proof: Proof. exact: (iffP forall_inP). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition