proposition: Lemma mem_pblockC (T : finType) (P : {set {set T}}) : trivIset P -> forall x y : T, (x \in pblock P y) = (y \in pblock P x).
proof: Proof. move=> Htriv. suff refl x y : x \in pblock P y -> y \in pblock P x. by move=> x y; apply/(sameP idP)/(iffP idP); apply refl. move=> /[dup] /(same_pblock Htriv) eqPxy. rewrite -eqPxy mem_pblock => Hcov. by rewrite -eq_pblock // eqPxy. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition