proposition: Fact meet_finerP R P Q : (R <= meet_finer P Q)%O = (R <= P)%O && (R <= Q)%O.
proof: Proof. apply/idP/andP=> [Hmeet | [/is_finerP RA /is_finerP RB]]. split; apply: (le_trans Hmeet); first exact: le_meet_finer. by rewrite meet_finerC le_meet_finer. apply/is_finerP=> X XinR. move/(_ X XinR): RA=> [A AinP XsA]. move/(_ X XinR): RB=> [B BinQ XsB]. exists (A :&: B); last by rewrite subsetI XsA XsB. apply/mem_meet_finerP/(MeetSpec AinP BinQ)=> //. have {XsA XsB} XsAB : X \subset A :&: B by rewrite subsetI XsA XsB. apply: (subset_neq0 XsAB). by have /and3P[_ _]:= setpartP R; apply contra=> /eqP <-. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition