proposition: Lemma partition_ex C : C \in P -> exists x, C = pblock P x.
proof: Proof. move=> /[dup]/partition_neq0/set0Pn[x xC] CP. by exists x; apply/esym/def_pblock => //; have /and3P[] := D_partition. Qed.
imports: mathcomp(all_ssreflect) extra