proposition: Lemma le_meet_finer P Q : (meet_finer P Q <= P)%O.
proof: Proof. apply/is_finerP=> AB /mem_meet_finerP[/= A B ainP BinQ Ineq0 ->{AB}]. by exists A; last exact: subsetIl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition