proposition: Lemma mem_meet_finerP P Q X : reflect (meet_spec P Q X) (X \in meet_finer P Q).
proof: Proof. apply (iffP imset2P)=> [[/= A B AinP]|]. rewrite inE=> /andP[BinQ ABneq0 ->{X}]. exact: (MeetSpec AinP BinQ). move=> [A B AinP BinQ ABneq0 ->{X}]. by exists A B=> //; rewrite inE; apply/andP. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition