proposition: Lemma is_finer_subpartP P Q : reflect (exists2 subpart : {set T} -> {set {set T}}, forall B, B \in Q -> partition (subpart B) B & \bigcup_(B in Q) subpart B = P) (P <= Q)%O.
proof: Proof. apply (iffP idP) => [PfinQ | [f partf UeqP]]; first last. apply/is_finerP=> A; rewrite -UeqP=> /bigcupP[/= B BinQ AinfB]. exists B; first exact: BinQ. move/(_ B BinQ): partf=> /cover_partition <-. exact: (bigcup_max _ AinfB). exists (fun B => [set A | (A \in P) && (A \subset B)]). - move=> B BinQ; apply/and3P; split. + rewrite eqEsubset; apply/andP; split. by apply/bigcupsP=> C; rewrite inE=> /andP[]. apply/subsetP=> x xinB. have xinS : x \in S by apply: (subsetP (setpart_subset BinQ)). apply/bigcupP; exists (pblock P x); first last. by rewrite mem_pblock cover_setpart. rewrite inE (pblock_in _ (setpart_non0 _)) cover_setpart xinS /=. suff <- : pblock Q x = B by apply: (is_finer_pblockP P Q PfinQ). exact: def_pblock. + apply: (trivIsetS _ (trivIsetpart P)). by apply/subsetP=> x; rewrite inE=> /andP[]. + by have:= setpart_non0 P; apply contra; rewrite inE=> /andP[]. - apply/setP=> /= A; apply/bigcupP/idP=> /= [[B BinQ] | AinP]. + by rewrite inE=> /andP[]. + move/is_finerP: PfinQ=> /(_ A AinP) [B BinQ AsB]. by exists B=> //; rewrite inE AinP AsB. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition