proposition: Lemma is_finer_card : #|Q| <= #|P| ?= iff (P == Q).
proof: Proof. split; first by rewrite -image_map_finer leq_imset_card. apply/eqP/eqP=> [|-> //]. rewrite -image_map_finer => /eqP/imset_injP map_finer_inj. apply val_inj => /=; rewrite -image_map_finer. suff : {in P, map_finer =1 id} by move/eq_in_imset => ->; rewrite imset_id. move=> /= A /[dup] AinP /mem_setpart_pblock [x xinA]. apply/eqP; rewrite eqEsubset map_finer_subset // andbT. rewrite -(mem_eq_pblock AinP xinA) map_finer_pblock. apply/subsetP => y /(same_pblock (trivIsetpart Q)) Qxy. have xinS : x \in S by apply: (subsetP (setpart_subset AinP)). have yinS : y \in S. rewrite -(cover_setpart Q) -mem_pblock Qxy. by rewrite -eq_pblock ?cover_setpart ?Qxy. rewrite -eq_pblock ?cover_setpart //. apply/eqP/esym; move: Qxy; rewrite -!map_finer_pblock. by apply: map_finer_inj; apply: pblock_mem; rewrite cover_setpart. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition