proposition: Lemma eq_pblock P x y : trivIset P -> x \in cover P -> (pblock P x == pblock P y) = (y \in pblock P x).
proof: Proof. move=> tiP Px; apply/eqP/idP=> [eq_xy | /same_pblock-> //]. move: Px; rewrite -mem_pblock eq_xy /pblock. by case: pickP => [B /andP[] // | _] /[1!inE]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)