proposition: Fact meet_finer_subproof P Q : partition [set A :&: B | A in P, B in Q & A :&: B != set0] S.
proof: Proof. apply/and3P; split. - apply/eqP/setP=> x; apply/bigcupP/idP=> [| xinS /=]. + move=> [/= y /imset2P[/= A B AinP]]. rewrite inE=> /andP[BinQ _ ->{y}]; rewrite inE=> /andP[_]. exact/subsetP/(setpart_subset BinQ). + have xinU : x \in pblock P x :&: pblock Q x. by rewrite inE !mem_pblock !cover_setpart xinS. exists (pblock P x :&: pblock Q x); last exact xinU. apply: imset2_f; first by apply pblock_mem; rewrite cover_setpart. rewrite inE pblock_mem ?cover_setpart //=. by apply/set0Pn; exists x. - apply/trivIsetP=> AB1 AB2. move=> /imset2P[/= A1 B1 A1inP]; rewrite inE=> /andP[B1inQ _ ->{AB1}]. move=> /imset2P[/= A2 B2 A2inP]; rewrite inE=> /andP[B2inQ _ ->{AB2}]. apply contraR; rewrite -setI_eq0=> /set0Pn[x]. rewrite !inE=> /andP[/andP[xinA1 xinB1] /andP[xinA2 xinB2]]. suff [-> ->] : A1 = A2 /\ B1 = B2 by []. split; first exact: (setpart_eq A1inP A2inP xinA1 xinA2). exact: (setpart_eq B1inQ B2inQ xinB1 xinB2). - apply/negP=> /imset2P[/= A B _]. by rewrite inE=> /andP[_] + H; rewrite H eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition