proposition: Lemma Bell_rec n: natp n -> Bell_number (csucc n) = csumb (Nintc n) (fun k => (binom n k) *c (Bell_number k)).
proof: Proof. move => nN. set E := Nint (csucc n); set X := (partitions E). set E' := (Nint n). have nE: inc n E by apply: Nint_si. have ce: cardinal E = csucc n by rewrite (card_Nint (NS_succ nN)). have ce1: cardinal E' = n by rewrite (card_Nint nN). have see': sub E' E by apply:Nint_M. pose fb p := select (fun s => inc n s) p. have prb: forall p, inc p X -> inc n (fb p) /\ inc (fb p) p. move => t /Zo_P [_] [[pa pc] pb]; apply: (select_pr). move: nE; rewrite -pa; move /setU_P => [y sa sb]; ex_tac. move => x y xp nx yp ny; case: (pc _ _ xp yp) => // bad; empty_tac1 n. have fcq: forall p, inc p X -> cardinal (fb p -s1 n) <=c n. move => p pX; move: (prb _ pX) => [pa pb]. move /Zo_P: pX => [] /setP_P h _. move: (h _ pb) => /setP_P => /(sub_smaller); rewrite ce - (cpred_pr5 pa)=>w. case: (equal_or_not (cardinal (fb p)) \0c) => e1. rewrite e1 cpred0; apply: (cle0n nN). apply/(cleSSP); fprops; first by apply:CS_pred;fprops. by rewrite - (proj2(cpred_pr (NS_le_nat w (NS_succ nN)) e1)). pose fc p := n -c cardinal (fb p -s1 n). have fcp: forall p, inc p X-> inc (fc p) (Nintc n). move => p pX; apply /(NintcP nN); apply:cdiff_le1; fprops. rewrite /Bell_number (card_partition_induced fcp); apply: csumb_exten. move => k /(NintcP nN) kn. have kN:= (NS_le_nat kn nN). rewrite (binom_symmetric nN kn). rewrite -(card_p_subsets nN (NS_diff k nN) ce1). set E1 := Zo _ _; set K1 := subsets_with_p_elements _ _. pose phi := Lf (fun z => (fb z -s1 n)) E1 K1. have pc: forall c, inc c E1 -> inc (fb c -s1 n) K1. move => x /Zo_P [pa pb]; apply /Zo_P;split => //. apply /setP_P => t /setC1_P [pc pd]; apply /(NintP nN); split => //. move: (pa) => /Zo_S /setP_P sb; move /setP_P:(sb _ (proj2 (prb _ pa))). by move =>sc; move /(NintsP nN): (sc _ pc). by rewrite -pb /fc double_diff //; apply: fcq. have sphi: E1 = source phi by rewrite /phi; aw. have tphi: K1 = target phi by rewrite /phi; aw. have fphi: function phi by apply: lf_function. rewrite sphi tphi; apply: (shepherd_principle fphi). rewrite - tphi => S /Zo_P [] /setP_P sa sb. have ->: (Vfi1 phi S) = Zo X (fun z => fb z -s1 n = S). set_extens t. move /(iim_fun_set1_P _ fphi); rewrite - sphi; move => [s1]. by rewrite /phi LfV// => s2; apply /Zo_P;split => //; move /Zo_P: s1 => []. move => /Zo_P [s1 s2]; apply /(iim_fun_set1_P _ fphi). have te1: inc t E1. by apply /Zo_P;split => //; rewrite /fc s2 sb double_diff. by rewrite - sphi /phi;split => //;rewrite LfV. have sc: E -s (S +s1 n) = E' -s S. set_extens t. move => /setC_P [te] /setU1_P h; apply /setC_P. case: (equal_or_not t n) => tn; first by case: h; right. split; last by move => h1; case: h; left. by apply /(NintP nN); split => //; apply /(NintsP nN). move => /setC_P [t1 t2]; apply /setC_P; split; first by apply: see'. by apply /setU1_P; case => // tn; move /(NintP nN) : t1 => []. have sd: k = n -c cardinal S by rewrite sb double_diff. pose E'':= (E -s (S +s1 n)). have se: cardinal E'' = k. have fse': finite_set E' by apply /NatP; rewrite (card_Nint nN). by rewrite /E'' sc (cardinal_setC4 sa fse') ce1 sd. rewrite -/(Bell_number k) - se - Bell_pr2; last by apply/NatP; rewrite se. symmetry; apply/ card_eqP. set A:= partitions E''; set B := Zo _ _. pose f p := p +s1 (S +s1 n). have pa: forall p, inc p A -> inc (f p) (\Po (\Po E)). move => p /Zo_P [p1 [[p2 p4] p3]]; apply /setP_P => t /setU1_P; case. move => tp; apply /setP_P => s st. move/setP_P: p1 => h1; move: (h1 _ tp) => h2; move/setP_P: h2 => h3. by move: (h3 _ st) => /setC_P []. move => ->; apply /setP_P => s /setU1_P; case; fprops. move => ->; apply :(Nint_si nN). have pb: forall p, inc p A -> inc (f p) X. move => p pA; move: (pa _ pA) => pn; apply /Zo_P; split => //. move /Zo_P: pA => [_] [[p1 p3] p2]; split; last first. move => t /setU1_P; case; [apply: p2 | move => ->; exists n; fprops]. split; first set_extens t. move => /setU_P [z tz zf]; move/setP_P: pn => h; move: (h _ zf). by move /setP_P; apply. move => te; case: (inc_or_not t (S +s1 n)) => h. by union_tac; apply /setU1_P; right. move: (setC_i te h); rewrite -/E'' -p1 => /setU_P [z za zb]. by union_tac; apply /setU1_P; left. move => a b /setU1_P; case => pb /setU1_P; case => pd. by apply: p3. right; rewrite pd; move: (setU_s1 pb); rewrite p1 => h. by apply: disjoint_pr => s sx; move: (h _ sx) => /setC_P []. right; rewrite pb; move: (setU_s1 pd); rewrite p1 => h. by apply: disjoint_pr => s sx sy; move: (h _ sy) => /setC_P []. by rewrite pb pd; left. have pd: forall p, inc p A -> fb (f p) = (S +s1 n). move => p pA; move: (pb _ pA) => h; move: (prb _ h) => [s1 s2]. case /setU1_P: s2 => // h1. move /Zo_P: pA => [] /setP_P ha _; move: (ha _ h1) => /setP_P => hb. by move: (hb _ s1) => /setC_P [_] /setU1_P; case; right. exists (Lf f A B); saw;apply: lf_bijective. move => p pA; apply /Zo_P;split; first by apply: pb. rewrite (pd _ pA); apply: setU1_K => ns; move: (sa _ ns). by move /(NintP nN) => []. move => u v uA vA sf. have aux: forall s, inc s A -> ~ inc (S +s1 n) s. move => s /Zo_P [] /setP_P h _ h1; move: (h _ h1) => /setP_P h2. have h3: inc n (S +s1 n) by fprops. by move: (h2 _ h3) => /setC_P []. by rewrite - (setU1_K (aux _ uA)) - (setU1_K (aux _ vA)) - /(f u) sf. move => y /Zo_P [p1 p2]; move: (prb _ p1) => [p3 p4]. have aux: S +s1 n = fb y by rewrite - p2;apply: setC1_K. exists (y -s1 (fb y)); last by symmetry;rewrite /f aux;apply: setC1_K. have q1: inc (y -s1 fb y) (\Po (\Po E'')). apply /setP_P => t /setC1_P [] ta tb; apply /setP_P => s st; apply /setC_P. move /Zo_P: p1 => [] /setP_P ha [[q1 q3] q2]; split. by move: (ha _ ta) => /setP_P; apply. move => h; case: (q3 _ _ p4 ta); rewrite /disjoint => h1; first by case: tb. by empty_tac1 s; apply /setI2_P; split => //; rewrite - aux. move /Zo_P: p1 => [_] [[q3 q5] q4]. apply /Zo_P;split => //; split; first split. move /setP_P: q1 => q2; set_extens t. by move /setU_P => [z za zb]; move: (q2 _ zb) => /setP_P; apply. move /setC_P => [t1 t2]; move: t1; rewrite -q3 => /setU_P [z z1 z2]. by union_tac; apply /setC1_P;split => //; move => h; case: t2; rewrite aux -h. by move => a b /setC1_P [s1 _] /setC1_P [s2 _]; apply: q5. by move => s /setC1_P [sy _]; apply:q4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)