proposition: Lemma same_pblock P x y : trivIset P -> x \in pblock P y -> pblock P x = pblock P y.
proof: Proof. rewrite {1 3}/pblock => tI; case: pickP => [A|]; last by rewrite inE. by case/andP=> PA _{y} /= Ax; apply: def_pblock. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)