proposition: Lemma pblock_equivalence P D : partition P D -> {in D & &, equivalence_rel (fun x y => y \in pblock P x)}.
proof: Proof. case/and3P=> /eqP <- tiP _ x y z Px Py Pz. by rewrite mem_pblock; split=> // /same_pblock->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)