proposition: Lemma partition_pigeonhole 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 => eq0. rewrite -!ltnNge -(setD1K BP) cardsU1 !inE eqxx /= add1n ltnS. have F (x : T) (xA : x \in A) : { C | (C \in P) & (x \in C) }. by apply/sig2W/bigcupP; rewrite -/(cover P) (cover_partition partP) subAD. pose f (x : T) : {set T} := if @idP (x \in A) is ReflectT xA then s2val (F _ xA) else set0. have inj_f : {in A &, injective f}. { move => x y; rewrite /f; case : {1}_ / idP => // xA _; case : {1}_ / idP => // yA _ E. case: (F x xA) E (s2valP' (F y yA)) => /= C CP xC <- yC. by have/card_le1_eqP/(_ y x) := sub1 _ CP; apply; apply/setIP. } rewrite -(card_in_imset inj_f); apply: subset_leq_card. apply/subsetP => ? /imsetP[x xA ->]; rewrite /f; move: xA. case : {1}_ / idP => // xA _; case: (F x xA) => /= C CP xC; rewrite !inE CP andbT. by apply: contraTneq eq0 => <-; apply/set0Pn; exists x; apply/setIP. Qed.
imports: mathcomp(all_ssreflect)