proposition: Lemma stirling_partition (T: finType) (E: {set T}) (p:nat): #|[set P | partition P E && (#|P| == p) ]| = 'St(#|E|, p).
proof: Proof. move: p; elim: {E} #|E| {1 3} E (refl_equal #|E|). move => E /cards0_eq => ->; case. apply: (eq_card1 (x := (@set0 {set T}))) => p. rewrite !inE cards_eq0 /= partition_set0; case : (p == set0) => //. move => n;apply: eq_card0 => p; rewrite !inE partition_set0 -cards_eq0. by apply /andP=> [[/eqP ->]]. move => n IHn E cE; case. apply: eq_card0 => P; rewrite !inE; apply /andP => [[/and3P[/eqP cP p1 _ ]]]. by rewrite cards_eq0 => /eqP p2; move: p1; rewrite/trivIset cP cE p2 big_set0. move => p. move: (ltn0Sn n); rewrite -cE card_gt0 => /set0Pn [xa xaE]. move: (setD1K xaE); set E' := E :\ xa => eq1. have xaE': xa \notin E' by rewrite !inE eqxx andFb. move: (sym_eq (cardsU1 xa E')); rewrite eq1 cE xaE' addnC addn1. move /eq_add_S => cE'; rewrite stirS - (IHn _ cE') - (IHn _ cE') {IHn}. rewrite - sum1dep_card (bigID (fun P => (pblock P xa == [set xa]))) /=. rewrite 2! sum1dep_card addnC; congr (_ + _). pose f x := ((pblock x xa) :\ xa |: (x :\ (pblock x xa))). set A := [set x | _]; set B := [set x | _]. have fAB: forall P (y := pblock P xa), P \in A -> (((f P) \in B) /\ (xa \in y /\ (y \in P) /\ (y :\ xa \notin P :\ y))). move => P y; rewrite !inE. move => /andP [/andP [/and3P [/eqP cP /trivIsetP tI eP] /eqP sP] yxa]. have yP: y \in P by apply: pblock_mem; rewrite cP. have xay: xa \in y by rewrite mem_pblock cP. have yane: y :\ xa != set0. apply: (contraNneq _ yxa); rewrite -/y -{2} (setD1K xay) => ->. by rewrite setU0 eqxx. have yanP: y :\ xa \notin P. apply /negP => y'P; move: (tI _ _ y'P yP (proper_neq (properD1 xay))). move /set0Pn: yane => [x /setD1P [xxa xy]] /pred0Pn. by case;exists x; rewrite /= !inE // xxa xy. have set0p: set0 \notin y :\ xa |: P :\ y. by rewrite !inE negb_or neq_sym yane negb_and eP orbT. have cy: cover (y :\ xa |: P :\ y) = E'. move: cP; rewrite -{1} (setD1K yP) /cover 2!bigcup_setU 2! big_set1 /E'. move => <-; apply /setP => x; rewrite in_setU 2! in_setD1 in_setU. apply /idP /idP; last by case /andP => ->; rewrite andTb. case /orP; first by move /andP => [-> ->] //. move => h; rewrite h orbT andbT; apply: contraTneq h => ->. rewrite /cover; apply/negP => /bigcupP [i] /setD1P [iy ip] xi. by move /pred0P: (tI _ _ ip yP iy) => h;move: (h xa) => /=;rewrite xay xi. have dia: forall s, s \in P :\ y -> y :\ xa != s -> [disjoint y :\ xa & s]. move => s /setD1P [sy sp] h1; move: (tI _ _ sp yP sy). rewrite - setI_eq0 => /eqP hh; apply /pred0P => t /=. by rewrite in_setD1 -andbA - in_setI setIC hh in_set0 andbF. have tIy: trivIset (y :\ xa |: P :\ y). apply /trivIsetP => s1 s2; case /setU1P => h1; case /setU1P => h2. - by rewrite h1 h2 eqxx. - by rewrite h1; apply: dia. - by rewrite neq_sym disjoint_sym h2; apply: dia. - by apply: tI; [ case /setD1P: h1 | case /setD1P: h2]. rewrite /partition set0p cy tIy eqxx 3!andTb. by rewrite cardsU1 -sP (cardsD1 y P) yP in_setD1 negb_and yanP orbT. pose g P y := ( xa |: y) |: (P :\ y). have fBA: forall P y, P \in B -> y \in P -> (g P y) \in A /\ f (g P y) = P. move => P y; rewrite !inE => /andP [/and3P [/eqP p1 p2 p3] /eqP p4] p5. move /trivIsetP: (p2) => tI; rewrite /partition. have xasP: forall s, s \in P -> xa \notin s. move => s sP; apply: contra xaE'=> xas; rewrite -p1. by apply /bigcupP; exists s. move: (xasP _ p5) => xay. have e1: (xa |: y \notin P :\ y). by rewrite in_setD1 negb_and (contra (xasP _)) ?orbT // setU11. have e2: xa |: y != [set xa]. by apply :contraNneq p3 => h; move: (setU1K xay); rewrite h setDv => ->. have dia: forall s, s \in P :\ y -> xa |: y != s -> [disjoint xa |: y & s]. move => s /setD1P [sy sp] us; move: (tI _ _ sp p5 sy). by rewrite disjointsU1 disjoint_sym (xasP _ sp) => ->. have e3: trivIset (xa |: y |: P :\ y). apply /trivIsetP => s1 s2; case /setU1P => h1; case /setU1P => h2. - by rewrite h1 h2 eqxx. - by rewrite h1; apply: dia. - by rewrite h2 disjoint_sym neq_sym; apply: dia. - by apply: tI; [ case /setD1P: h1 | case /setD1P: h2]. rewrite /g /f (def_pblock e3 (setU11 (xa |: y) (P :\ y))(setU11 xa y)). rewrite in_setU1 negb_or in_setD1 negb_and p3 orbT neq_sym -card_gt0. rewrite cardsU1 xay add1n ltn0Sn - p4 (cardsD1 y P) p5 cardsU1 e1 eqxx e2. rewrite (setU1K xay) (setU1K e1) (setD1K p5) e3 !andbT - eq1 - p1. by rewrite - {2} (setD1K p5) /cover 2!bigcup_setU 2! big_set1 setUA. have -> : B = f @: A. apply /setP => y; apply /idP/idP. move => yb; move: (yb); rewrite inE => /andP [_] /eqP cy. move: (ltn0Sn p); rewrite -cy card_gt0 => /set0Pn [x xy]. move: (fBA _ _ yb xy) => [h1 <-]. by apply /imsetP; exists (g y x). move /imsetP => [P] pa ->; apply: (proj1 (fAB _ pa)). rewrite mulnC; apply:card_inv_im => x xA. move: (proj1 (fAB _ xA)); rewrite inE => /andP [_] /eqP => <-. set s := [set y | _]. have ->: s = g (f x) @: f x. apply /setP => t; rewrite inE; apply /idP/idP. move => /andP [ta /eqP sf]. move: (fAB _ ta); set y := pblock t xa ; move => [pa [pb [pc pd]]]. apply /imsetP; exists (y :\ xa); first by rewrite sf;apply/setU1P; left. by rewrite sf /f/g -/y (setD1K pb) (setU1K pd) (setD1K pc). move /imsetP => [z zf ->];move: (fBA _ _ (proj1 (fAB _ xA)) zf). by move => [-> ->]; rewrite eqxx. move: (fAB _ xA); set y := pblock x xa ; move => [pa [pb [pc pd]]]. rewrite (card_in_imset) // => u v p1 p2 eq. move: (fBA _ _ pa p1); rewrite inE => [][] /andP [] /andP []. move /and3P => [_ tI _] _ _ _. have p3 : pblock (g (f x) u) xa = xa |: u. have r2: xa |: u \in (g (f x) u) by apply /setU1P; left. by rewrite (def_pblock tI r2) // setU11. have p4 : pblock (g (f x) v) xa = xa |: v. rewrite eq in tI. have r2: xa |: v \in (g (f x) v) by apply /setU1P; left. by rewrite (def_pblock tI r2) // setU11. have xau: forall u, u \in f x -> xa \notin u. move: pa; rewrite inE => /andP [] /and3P [/eqP cf _ _] _. move => w wf; apply/negP => xaw; move /negP:xaE'; rewrite -cf /cover. by case; apply /bigcupP; exists w. have ->: u = (xa |: u) :\ xa by rewrite setU1K //; apply: xau. have ->: v = (xa |: v) :\ xa by rewrite setU1K //; apply: xau. by rewrite -p3 -p4 eq. have aux: forall P, partition P E' -> [set xa] \notin P. move => P /and3P [] /eqP pa pb pc; apply /negP => pd. move/negP: xaE'; case; rewrite -pa. apply /bigcupP; exists [set xa] => //; apply: set11. have h: {in [set P | partition P E' && (#|P| == p)] &, injective (fun P => [set xa] |: P)}. move => P Q; rewrite !inE => /andP [p1 _] /andP [p2 _] eq. by rewrite - (setU1K (aux _ p1)) - (setU1K (aux _ p2)) eq. rewrite -(card_in_imset h) {h}; apply: eq_card => y; rewrite !inE. apply /idP/idP. move /andP =>[] /andP [] /and3P [] /eqP uy ty ey /eqP cy /eqP uy'. move: xaE; rewrite - uy => xay. move: (pblock_mem xay); rewrite uy' => xsay; move: (setD1K xsay) => h. apply /imsetP; exists (y :\ [set xa]) => //. move: (cardsU1 [set xa] (y :\ [set xa])); rewrite h setD11 add1n cy => cy'. rewrite inE -eqSS -cy' eqxx andbT /partition in_setD1 negb_and ey orbT andbT. apply /andP; split. rewrite /E' - uy - {2} h; rewrite /cover bigcup_setU big_set1 setU1K //. apply /negP => /bigcupP => [] [i] /setD1P [iny iy] xai. move /trivIsetP: ty => hh; move: (hh _ _ iy xsay iny). by rewrite disjoint_sym disjoints_subset sub1set; move /setCP; case. apply /trivIsetP => x x' /setD1P [] _ xy /setD1P [] _; move: xy. move /trivIsetP: ty; apply. move /imsetP => [x]; rewrite inE => /andP [px] /eqP cx -> {y}. move /and3P: px => [] /eqP ux tx ex. have pf: {in x, forall B : {set T}, [disjoint [set xa] & B]}. move => s sy /=; rewrite (eq_disjoint1 (x:= xa)). apply /negP => xas. by move: xaE'; rewrite -ux; move /negP; case; apply /bigcupP; exists s. by move => u; rewrite !inE. move: (trivIsetU1 pf tx ex) => [qa qb]. rewrite /partition cardsU1 qa qb cx add1n. rewrite (def_pblock qa (setU11 [set xa] x))? set11//. rewrite /cover bigcup_setU big_set1 -/(cover x) ux eq1. rewrite in_setU1 negb_or ex !eqxx ! andbT !andTb; apply /negP => /eqP h. have // : 0 = 1 by rewrite - {1} (@cards0 T) h cards1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)