proposition: Lemma is_finerP P Q : reflect (forall A, A \in P -> exists2 B : {set T}, B \in Q & A \subset B) (P <= Q)%O.
proof: Proof. apply (iffP (is_finer_pblockP P Q)) => [subPQ A AinP | H x xinS]. have [x xinA] := mem_setpart_pblock AinP. have Aeq := mem_eq_pblock AinP xinA; subst A. exists (pblock Q x); last exact/subPQ/(subsetP (setpart_subset AinP)). by rewrite pblock_in // (cover_setpart Q) (subsetP (setpart_subset AinP)). apply/subsetP => y yPx. have eqPxy := same_pblock (trivIsetpart P) yPx. have:= yPx; rewrite -eqPxy mem_pblock=> /pblock_mem{}/H[A AinQ /subsetP PsA]. suff -> : pblock Q x = A by apply: PsA; rewrite eqPxy. apply: (def_pblock (trivIsetpart Q) AinQ). by apply: PsA; rewrite eqPxy mem_pblock cover_setpart. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition