proposition: Lemma mem_preim_partition (B : {set T}) : B \in preim_partition f D -> exists x0 : T, (x0 \in B) /\ (B = D :&: f @^-1: [set f x0]).
proof: Proof. move=> HB. have /and3P[/eqP Hcov Htriv notP0] := preim_partitionP f D. have /set0Pn[x Bx] := memPn notP0 B HB. have Hx : x \in D by rewrite -Hcov; apply/bigcupP; exists B. have Bblock : pblock (preim_partition f D) x = B by apply def_pblock. exists x; split => //; apply/setP => y; rewrite inE -Bblock. case/boolP: (y \in D) => /= Hy; first last. - apply negbTE; move: Hy; apply contra => Hy. rewrite -Hcov; apply/bigcupP; exists B => //. by rewrite -Bblock. - by rewrite inE pblock_equivalence_partition ?inE //; split => // /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree