proposition: Lemma nbsurj_part n p: natp n -> natp p -> nbsurj n p = (factorial p) *c (nbpart n p).
proof: Proof. move => nN pN. rewrite /nbsurj /nbpart. set I := (Nint n); set J:= (Nint p). have cj: p = cardinal J by rewrite (card_Nint pN). set E := (surjections I J). set K := (partitionsx I p). pose f g := fun_image J (fun z => Vfi1 g z). have lfa: lf_axiom f E K. move => g /Zo_P [] /functionsP [fg sg tg] sjg. have p1: inc (f g) (\Po (\Po I)). apply /setP_P => z /funI_P [w wJ ->]; apply /setP_P => t. by move /(iim_fun_set1_P w fg) => []; rewrite sg. have p2: cardinal (f g) = p. symmetry; rewrite cj; apply /card_eqP. exists (Lf (fun z => Vfi1 g z) J (f g)). saw; apply lf_bijective. move => z zj; apply /funI_P; ex_tac. move => u v uj vj si. rewrite -tg in uj; move: (proj2 sjg _ uj) => [x xsg h]. move: (iim_fun_set1_i fg xsg h); rewrite si => xi. by rewrite (iim_fun_set1_hi fg xi) - h. by move => y /funI_P. have p3: union (f g) = I. set_extens t. move =>/setU_P [z tz h]; move /setP_P: p1 => h1. by move: (h1 _ h) => /setP_P; apply. move => ti; apply /setU_P; exists (Vfi1 g (Vf g t)). rewrite - sg in ti. by exact: (iim_fun_set1_i fg ti (refl_equal (Vf g t))). apply /funI_P; exists (Vf g t) => //; rewrite -tg; Wtac. have p4: alls (f g) nonempty. move => z /funI_P [t]; rewrite - tg => ttg ->. move: (proj2 sjg _ ttg) => [x xsg h]. move: (iim_fun_set1_i fg xsg h) => h1; ex_tac. apply /Zo_P; split => //; apply:Zo_i => //;split => //; split => //. move => a b a1 b1; mdi_tac nab => u ua ub; case: nab; move: ua ub. move /funI_P: a1 => [z zj ->]; move /funI_P: b1 => [w wj ->]. by move => h1 h2;rewrite (iim_fun_set1_hi fg h1) - (iim_fun_set1_hi fg h2). pose phi := Lf f E K. have sphi: E = source phi by rewrite /phi; aw. have ->: K = target phi by rewrite /phi; aw. have fphi: function phi by apply: lf_function. rewrite sphi cprodC; apply: (shepherd_principle fphi). rewrite {1} /phi; aw; move => x xK. set F := Vfi1 phi x. have fp: forall g, inc g F <-> inc g (surjections I J) /\ f g = x. move => g; split. move /(iim_fun_set1_P _ fphi) => []; rewrite - sphi => fe;rewrite{1}/phi. rewrite LfV//; move => pa;split => //. move => [pa pb]; apply /(iim_fun_set1_P _ fphi). by split => //;[ ue | rewrite /phi LfV//]. move: (xK) => /Zo_P [px]; rewrite cj. move /card_eqP => [fa [bfa sfa tfa]]. move /Zo_hi: px => [[pa pb] pc]. pose fb t := select (inc t) x. have prb: forall t, inc t I -> inc t (fb t) /\ inc (fb t) x. move => t ti; apply: (select_pr). move: ti; rewrite - pa => /setU_P [z za zb]; ex_tac. move => a b sa sb sc sd; case: (pb _ _ sa sc) => // h; empty_tac1 t. pose fc := Lf (fun t => (Vf fa (fb t))) I J. have sfc: source fc = I by rewrite /fc; aw. have tfc: target fc = J by rewrite /fc; aw. have fc0: lf_axiom (fun t => (Vf fa (fb t))) I J. move=> t ti; move: (prb _ ti) => [_]; rewrite - sfa - tfa => h; Wtac;fct_tac. have fc1: function fc by apply: lf_function. have fc2': surjection fc. split => // y; rewrite /fc; aw; rewrite - tfa => yJ. move: (bij_surj bfa yJ); rewrite sfa; move => [z zx ->]. move: (pc _ zx) => [t tz]. have ti: inc t I by rewrite - pa; union_tac. rewrite tfa;ex_tac; rewrite LfV//. move: (prb _ ti) => [sa sb]; case: (pb _ _ zx sb); first by move => ->. move => h; empty_tac1 t. have fc2: inc fc (surjections I J). apply /Zo_P; split => //; by apply /functionsP. have fc3: forall w, inc w x -> Vfi1 fc (Vf fa w) = w. move => w wx; set_extens s. move /(iim_fun_set1_P _ fc1); rewrite sfc /fc; move => [ta]; rewrite LfV//. move => vfa; move: (prb _ ta) => [tb tc]. by rewrite - sfa in wx tc; rewrite (bij_inj bfa wx tc vfa). move => sw; apply /(iim_fun_set1_P _ fc1). have si: inc s I by rewrite - pa; union_tac. rewrite sfc /fc LfV//;split => //; move: (prb _ si) => [tb tc]. case: (pb _ _ wx tc); [by move => <- | by move =>h; empty_tac1 s]. have fc4: inc fc F. move: (proj1 (proj1 bfa)) => ffa. apply /fp; split => //; rewrite /f;set_extens t. move /funI_P => [z zJ ->]; rewrite -tfa in zJ. move: (bij_surj bfa zJ); rewrite sfa; move => [w wx ->]. by rewrite (fc3 _ wx). move => tx; apply /funI_P; exists (Vf fa t); first by Wtac. by rewrite (fc3 _ tx). rewrite - (card_permutations (finite_Nint p)). symmetry; apply /card_eqP. exists (Lf (fun z => z \co fc) (permutations J) F); saw. move /Zo_P: (fc2) => [sa sb]; move: (exists_right_inv_from_surj sb) => [s sc]. apply /lf_bijective. move => g /Zo_P [] /functionsP [fg sg tg] big. have gfc: g \coP fc by split => //; rewrite sg tfc. have fgfc: function (g \co fc) by fct_tac. have tgfc: target (g \co fc) = J by aw. have sgfc: source (g \co fc) = I by aw. have ssgfc: surjection(g \co fc) by apply/compose_fs =>//;exact (proj2 big). have pa':inc (g \co fc) (surjections I J). apply /Zo_P; split; first by apply/functionsP;aw. by apply /compose_fs => //; exact (proj2 big). have aux2: forall w, inc w I -> (Vfi1 (g \co fc) (Vf (g \co fc) w)) = (Vfi1 fc (Vf fc w)). move => w wi; set_extens t. move /(iim_fun_set1_P _ fgfc); rewrite sgfc; move => [tI]. rewrite - sfc in wi tI; rewrite ! compfV//. move: (Vf_target fc1 wi) (Vf_target fc1 tI); rewrite tfc - sg. move => i1 i2 i3; rewrite (bij_inj big i1 i2 i3). by apply: (iim_fun_set1_i fc1 tI). rewrite - sfc in wi; move /(iim_fun_set1_P _ fc1) => [ta tb]. rewrite compfV //; apply:(iim_fun_set1_i fgfc); aw; trivial. rewrite compfV//; ue. move /fp: fc4 => [_] xv1. apply /fp;split => //; set_extens t. move /funI_P => [z zJ ->]. rewrite -tgfc in zJ; move: (proj2 ssgfc _ zJ); rewrite sgfc. move => [a ai ->]; rewrite (aux2 _ ai) - xv1. apply /funI_P;exists (Vf fc a) => //; Wtac. rewrite -xv1; move /funI_P => [z zj etc]. apply /funI_P; rewrite -tfc in zj; move: (proj2 fc2' _ zj) etc. move => [a]; rewrite sfc => s1 ->; rewrite - (aux2 _ s1) => ->. exists (Vf (g \co fc) a) => //; rewrite - tgfc; Wtac. move => u v up vp sv; move: sc => [sc sd]. move: up vp sa => /Zo_P [] /functionsP [fu su tu] _ /Zo_P [] /functionsP. move => [fv srv tv] _ /functionsP [fs sss ts]. have c1: u \coP fc by split => //; ue. have c2: v \coP fc by split => //; ue. move: (f_equal (fun z => z \co s) sv). by rewrite - !compfA // sd ts - {1} su (compf_id_r fu) - srv (compf_id_r fv). move => y yf. move /fp: yf => [] /Zo_P []/functionsP [fy sy ty] sjy fyv. move /Zo_P: fc2 => [_ sj1]. have sysj: source y = source fc by ue. have aux: forall x0 y0 : Set, inc x0 (source fc) -> inc y0 (source fc) -> Vf fc x0 = Vf fc y0 -> Vf y x0 = Vf y y0. rewrite sfc; move => a b aI bI; rewrite /fc ! LfV// => sv. move: (prb _ aI)(prb _ bI) => [s1 s2] [s3 s4]. rewrite - sfa in s2 s4; move: (bij_inj bfa s2 s4 sv) => sf. move: s2; rewrite sfa - fyv; move /funI_P => [z zj] => ta. move: s1; rewrite ta => s1; rewrite - (iim_fun_set1_hi fy s1). by move: s3; rewrite - sf ta => s2; rewrite (iim_fun_set1_hi fy s2). set h:= y \co s. have pr1: fc \coP s by move:sc => [s1 s2]. have pr2: y \coP s by red;move: pr1 => [s1 s2 <-]. move:(sc) => [[_ s2 s3] s4]. have fh: function h by rewrite /h; fct_tac => //; rewrite sy - s3 sfc. move: (f_equal source s4); aw; rewrite tfc => srs. have hf: inc h (functions J J). by apply /functionsP; red; rewrite {2 3} /h; aw. have sjh: surjection h. split => // y1; rewrite /h; aw => y1y; move: (proj2 sjy _ y1y). rewrite sy srs; move => [a ai ->]. set b := Vf fc a; have bj: inc b J by rewrite - tfc /b; Wtac. have bs: inc b (source s) by ue. have bs3: inc (Vf s b) I by rewrite - sfc s3; Wtac. ex_tac; rewrite compfV//; apply: aux; rewrite ? sfc //. move: (f_equal (Vf^~ b) s4); rewrite compfV // idV //; ue. have bh: bijection h. move /functionsP: hf => [_ sh th]. apply: bijective_if_same_finite_c_surj; rewrite ? sh ? th=> //. by red; rewrite - cj; apply /NatP. rewrite -(left_composable_value fy sj1 sysj aux sc (refl_equal h)). by exists h=> //;apply /Zo_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)