proposition: Lemma partition_pigeonhole P D A : partition P D -> #|P| <= #|A| -> A \subset D -> {in P, forall B, #|A :&: B| <= 1} -> {in P, forall B, A :&: B != set0}.
proof: Proof. move=> partP card_A_P /subsetP subAD sub1; apply/forall_inP. apply: contraTT card_A_P => /forall_inPn [B BP]; rewrite negbK => AB0. rewrite -!ltnNge -(setD1K BP) cardsU1 !inE eqxx /= add1n ltnS. have [tP covP] := (partition_trivIset partP,cover_partition partP). have APx x : x \in A -> x \in pblock P x by rewrite mem_pblock covP; apply: subAD. have inj_f : {in A &, injective (pblock P)}. move=> x y xA yA /eqP; rewrite eq_pblock ?covP ?subAD // => Pxy. apply: (@card_le1_eqP _ (A :&: pblock P x)); rewrite ?inE ?Pxy ?APx ?andbT //. by apply: sub1; rewrite pblock_mem ?covP ?subAD. rewrite -(card_in_imset inj_f); apply: subset_leq_card. apply/subsetP => ? /imsetP[x xA ->]. rewrite !inE pblock_mem ?covP ?subAD ?andbT //. by apply: contraTneq AB0 => <-; apply/set0Pn; exists x; rewrite inE APx ?andbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)