proposition: Lemma map_finer_pblock x : map_finer (pblock P x) = pblock Q x.
proof: Proof. rewrite /map_finer; case (boolP (pblock P x \in P)) => [H |]; first last. rewrite (pblock_in _ (setpart_non0 P)) (cover_setpart P). by rewrite -(pblock_notin Q) negbK => /eqP->. case: (sig2W _) => /= B BinQ /subsetP PxB. apply esym; apply def_pblock => //. by apply PxB; rewrite mem_pblock -pblock_in. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition