proposition: Lemma image_map_finer : [set map_finer x | x in P] = Q.
proof: Proof. apply/setP=> /= B; apply/imsetP/idP=> /=[[A /map_finer_in H ->{B}] // |]. move=> /[dup] BinQ /mem_setpart_pblock=> -[x xinB]; exists (pblock P x). apply pblock_mem; rewrite cover_setpart. exact: (subsetP (setpart_subset BinQ)). by apply esym; rewrite map_finer_pblock; apply: def_pblock. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition