proposition: Lemma equivalence_partition_pblock P D : partition P D -> equivalence_partition (fun x y => y \in pblock P x) D = P.
proof: Proof. case/and3P=> /eqP <-{D} tiP notP0; apply/setP=> B /=; set D := cover P. have defP x: x \in D -> [set y in D | y \in pblock P x] = pblock P x. by move=> Dx; apply/setIidPr; rewrite (bigcup_max (pblock P x)) ?pblock_mem. apply/imsetP/idP=> [[x Px ->{B}] | PB]; first by rewrite defP ?pblock_mem. have /set0Pn[x Bx]: B != set0 := memPn notP0 B PB. have Px: x \in cover P by apply/bigcupP; exists B. by exists x; rewrite // defP // (def_pblock tiP PB Bx). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)