proposition: Fact is_finer_setpart_anti : antisymmetric is_finer.
proof: Proof. suff finsub P Q : is_finer P Q -> is_finer Q P -> P \subset Q. move=> P Q /andP[finPQ finQP]. apply/eqP; rewrite eqE /=; rewrite eqEsubset. by apply/andP; split; apply: finsub. move=> /is_finer_pblockP PsQ /is_finer_pblockP QsP. apply/subsetP=> /= A AinP. have [x xinA] := mem_setpart_pblock AinP. have Aeq := mem_eq_pblock AinP xinA; subst A. have xinS : x \in S by apply: (subsetP (setpart_subset AinP)). have -> : pblock P x = pblock Q x. by apply/eqP; rewrite eqEsubset ?PsQ ?QsP. by apply pblock_mem; rewrite (cover_setpart Q). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition