proposition: Lemma nbdr_pr1 n:natp n -> factorial n = csumb (Nintc n) (fun k => binom n k *c nbder k).
proof: Proof. move => nN. set I := (Nint n). have caI : cardinal I = n by rewrite (card_Nint nN). have fsi: finite_set I by apply: finite_Nint. move: (card_permutations fsi); rewrite - caI => <-. pose g f := Zo I (fun x => Vf f x <> x). pose Xk k := Zo (permutations I) (fun z => cardinal (g z) = k). set X := Lg (Nintc n) Xk. have X1: fgraph X by rewrite /X; fprops. have X2: mutually_disjoint X. red;rewrite /X;aw => i j ip jp; rewrite ! LgV//;mdi_tac nij => u ua ub; case: nij. by move: ua ub => /Zo_P [_ <- ] /Zo_P [_ <-]. have X3: (unionb X) = (permutations I). rewrite /X;set_extens t. move /setUb_P; aw; move => [y yp]; rewrite LgV//; move /Zo_P => [p1 p2] //. have sa: inc (cardinal (g t)) (Nintc n). have h: sub (g t) I by apply: Zo_S. apply /NintcP => //; rewrite - caI; apply: (sub_smaller h). move => ti; apply /setUb_P; aw;exists (cardinal (g t)) => //. rewrite /Xk LgV// ;apply /Zo_P;split => //. move: (csum_pr4 X2); rewrite X3 => ->. rewrite {1} /X /csumb caI; aw; apply: csumb_exten. move => k kn; rewrite /X LgV//; move/(NintcP nN): kn => kn;clear X X1 X2 X3. have kN:= (NS_le_nat kn nN). rewrite - (card_p_subsets nN kN caI). set K := (subsets_with_p_elements k I). pose phi := Lf g (Xk k) K. have sphi: (Xk k) = source phi by rewrite /phi; aw. have ->: K = target phi by rewrite /phi; aw. have ta: lf_axiom g (Xk k) K. by move => f /Zo_P [p1 p2]; apply/Zo_P;split => //; apply/setP_P; apply: Zo_S. have fphi: function phi by apply: lf_function. rewrite sphi; apply: (shepherd_principle fphi). rewrite {1} /phi; aw; move => x xK. set W := (Vfi1 phi x). have kp: forall f, inc f W <-> inc f (Xk k) /\ g f = x. move => f; split. by move/(iim_fun_set1_P _ fphi); rewrite - sphi /phi; move => [h];rewrite LfV// => h1. move => [pa pb]; apply/(iim_fun_set1_P _ fphi). have fsp: inc f (source phi) by rewrite - sphi. by rewrite /phi LfV. move: (xK) => /Zo_P [] /setP_P sxi cx. pose r f := Lf (Vf f) x x. have pa: forall f, inc f W -> [/\ lf_axiom (Vf f) x x, (forall t, inc t x -> Vf (r f) t = Vf f t), (forall t, inc t (I -s x) -> Vf f t = t) & inc (r f) (derangements x)]. move => f /kp [] /Zo_P [] /Zo_P [] /functionsP [ff sf tf] bf fp gf. have lfa: lf_axiom (Vf f) x x. move => s st; move: (st); rewrite - gf => /Zo_P [si siv]. have ax: inc (Vf f s) I by rewrite - tf; Wtac. apply /Zo_P;split => // => sv; rewrite - sf in si ax. by move:(bij_inj bf ax si sv). have sv: forall t, inc t x -> Vf (r f) t = Vf f t. move => t tx; rewrite /r LfV//. have sv1:(forall t, inc t x -> Vf (r f) t <> t). by move => t tx; rewrite (sv _ tx); move: tx; rewrite - gf => /Zo_P []. have sv2: (forall t : Set, inc t (I -s x) -> Vf f t = t). by move => t /setC_P [ti tx];ex_middle fx;case: tx;rewrite - gf; apply /Zo_P. rewrite /r;split => //; apply /Zo_P;split => //. apply /Zo_P;split => //. by apply /functionsP;saw; apply:lf_function. apply: lf_bijective => //. by move => u v ux vx; apply: (bij_inj bf); rewrite sf; apply: sxi. move => y yx. move: (sxi _ yx); rewrite -tf => ytf. move: (bij_surj bf ytf); rewrite sf; move => [z za zb]; exists z => //. by ex_middle zx; rewrite - (sv2 _ (setC_i za zx)) -zb. have ->: nbder k = cardinal (derangements x). have fsx: finite_set x by apply /NatP; rewrite cx. by rewrite (nbder_pr fsx) cx. apply /card_eqP; exists (Lf r W (derangements x)); saw. apply:lf_bijective. by move => t ts; move: (pa _ ts) => [_ _ _]. move => u v uw vw sr. move: (pa _ uw) (pa _ vw) => [_ p1 p2 _] [_ q1 q2 _]. move: uw => /kp [] /Zo_P [] /Zo_P [] /functionsP [f1 f2 f3] _ _ _. move: vw => /kp [] /Zo_P [] /Zo_P [] /functionsP [f1' f2' f3'] _ _ _. apply: function_exten => //; try ue. move => t ts; case: (inc_or_not t x) => tx. by rewrite - (p1 _ tx) - (q1 _ tx) sr. by rewrite f2 in ts; move : (setC_i ts tx) => h; rewrite (p2 _ h) (q2 _ h). move => y yd. move: yd => /Zo_P [] /Zo_P [] /functionsP [y1 y2 y3] y4 y5. set f := Lf (fun z => (Yo (inc z x) (Vf y z) z)) I I. have sa: forall z, inc z I -> inc ((Yo (inc z x) (Vf y z) z)) I. move => z zi; Ytac zx => //;apply: sxi; rewrite - y3; Wtac. have ff: function f by apply: lf_function. have gfx: g f = x. set_extens t. by move /Zo_P => [t1 t2]; ex_middle ntx; case: t2; rewrite /f LfV//; Ytac0. move => tx; move: (sxi _ tx) => ti. by apply /Zo_P;split => //;rewrite /f LfV//; Ytac0; apply: y5. have bf: bijection f. apply: lf_bijective. move => s; apply: sa. move => u v ui vi; case: (inc_or_not u x) => ux; Ytac0. case: (inc_or_not v x) => vx; Ytac0. by apply (bij_inj y4); rewrite y2. rewrite -y2 in ux; move: (Vf_target y1 ux); rewrite y3. by move => s1 s2; case: vx; rewrite - s2. case: (inc_or_not v x) => vx; Ytac0 => //. rewrite -y2 in vx; move: (Vf_target y1 vx); rewrite y3. by move => s1 s2; case: ux; rewrite s2. move => z zi; case: (inc_or_not z x). rewrite - {1} y3 => zy; move: (bij_surj y4 zy) => [t ]; rewrite y2. by move => tx ->; move: (sxi _ tx) => ti; ex_tac; Ytac0. by move => zx; ex_tac; Ytac0. have fp: inc f (permutations I) by rewrite/f;apply/permutationsP; saw. have rfy: r f = y. symmetry;rewrite /r/f. have aux: lf_axiom (Vf (Lf (fun z0 => Yo (inc z0 x) (Vf y z0) z0) I I)) x x. move => t tx;move: (sxi _ tx) => ti; rewrite LfV//;Ytac0;rewrite - y3; Wtac. apply: function_exten; aw;trivial; first by apply lf_function => //. by rewrite y2;move => s sx /=; move: (sxi _ sx) => si; rewrite !LfV//; Ytac0. by exists f => //; apply /kp;split => //; apply /Zo_P;split => //; rewrite gfx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)