proposition: Lemma pblock_inj : {in X &, injective (pblock P)}.
proof: Proof. by move=> x0; apply: (can_in_inj (pblockK x0)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)