proposition: Lemma preim_partition_pblock P D : partition P D -> preim_partition (pblock P) D = P.
proof: Proof. move=> partP; have [/eqP defD tiP _] := and3P partP. rewrite -{2}(equivalence_partition_pblock partP); apply: eq_in_imset => x Dx. by apply/setP=> y; rewrite !inE eq_pblock ?defD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)