proposition: Lemma pblock_equivalence_partition : {in D &, forall x y, (y \in pblock P x) = R x y}.
proof: Proof. have [_ tiP _] := and3P equivalence_partitionP. by move=> x y Dx Dy; rewrite /= (def_pblock tiP (PPx Dx) (Pxx Dx)) inE Dy. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)