proposition: Lemma meet_finerC : commutative meet_finer.
proof: Proof. suff incl P Q : meet_finer P Q \subset meet_finer Q P. by move=> P Q; apply/val_inj/eqP; rewrite eqEsubset !incl. apply/subsetP=> AB /mem_meet_finerP[A B AinP BinQ Ineq0 ->{AB}]. rewrite setIC; apply/mem_meet_finerP/(MeetSpec BinQ AinP)=> //. by rewrite setIC. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition