proposition: Lemma nbder_pr2 n: natp n -> nbder (csucc (csucc n)) = (csucc n) *c (nbder n +c nbder (csucc n)).
proof: Proof. move => nN. move: (NS_succ nN) => snN. move: (Nint_pr4 snN). set I :=Nint (csucc n); set I' := Nint (csucc (csucc n)). move => [pa pb]. have pc: inc (csucc n) I' by apply:Nint_si. have ci: cardinal I= csucc n by apply:(card_Nint snN). set G1 := (derangements I'). pose phi := Lf (Vf ^~(csucc n)) G1 I. have sp: G1 = source phi by rewrite /phi; aw. have tp: I = target phi by rewrite /phi; aw. have lfa: lf_axiom (Vf^~(csucc n)) G1 I. move => f /Zo_P [] /Zo_P [] /functionsP [ta tb tc] td te. move: (te _ pc) => bad; move: pc; rewrite -tb => pc. by move: (Vf_target ta pc); rewrite tc -pa; case /setU1_P. have fphi: function phi by apply: lf_function. have ci': cardinal I'= csucc (csucc n) by apply:(card_Nint (NS_succ snN)). have <-: cardinal (source phi) = nbder (csucc (csucc n)). rewrite - sp - ci'; apply:nbder_pr; red; rewrite ci'; apply /NatP; fprops. rewrite - {1} ci tp;apply:(shepherd_principle fphi). rewrite {1} /phi; aw; move => x xK. set G2 := Zo G1 (fun f => Vf f (csucc n) = x). have ->: Vfi1 phi x = G2. set_extens t. move/(iim_fun_set1_P _ fphi); rewrite - sp;move => [ts]. rewrite /phi /G2 LfV// => ->; apply /Zo_P;split => //. move => /Zo_P [tg1 <-]; apply /(iim_fun_set1_P _ fphi). rewrite /phi; aw; rewrite LfV//. set G3 := Zo G2 (fun f => Vf f x = (csucc n)). have sg3: sub G3 G2 by apply: Zo_S. have h0: csucc n <> x by move => h1; case: pb; rewrite h1. have fi: finite_set I' by apply: finite_Nint. have xi': inc x I' by rewrite - pa; fprops. rewrite (cardinal_setC2 sg3) - csum2cl - csum2cr; apply: f_equal2. set K := I -s1 x. have cK: n = cardinal K. by apply: csucc_inj; fprops; rewrite - ci (csucc_pr2 xK). have fsk: finite_set K by red; rewrite - cK; apply /NatP. rewrite cK - (nbder_pr fsk); apply /card_eqP. exists (Lf (fun f => (restriction2 f K K)) G3 (derangements K)). saw. have ski': sub K I' by rewrite -pa;move => t /setC_P [ti _]; fprops. have pd: forall f, inc f G3 -> restriction2_axioms f K K. move => f /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [] /functionsP [qa qb qc] qd qe qf qg. have ksf: sub K (source f) by ue. red; rewrite qb qc ;split => // t /(Vf_image_P qa ksf) [u uk ->]. move: (ksf _ uk) => usf; move: (Vf_target qa usf); rewrite qc -pa. have xsf: inc x (source f) by rewrite qb -pa; fprops. have nsf: inc (csucc n) (source f) by rewrite qb -pa; fprops. move /setC1_P: uk => [ui ux]; case /setU1_P => h. apply /setC1_P;split => // => h1; rewrite -h1 in qf. by move: (bij_inj qd nsf usf qf) => us; case: pb; rewrite us. by rewrite -h in qg; move: (bij_inj qd xsf usf qg) => xu; case: ux. apply: lf_bijective. move => f fg3; move: (pd _ fg3) => pe. set g := (restriction2 f K K). move: (restriction2_prop pe) => p0. have gs: inc g (functions K K) by apply /functionsP. move: p0 => [p1 p2 p3]. move: fg3 => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [] /functionsP [qa qb qc] qd qe qf qg. move: (restriction2_fi (proj1 qd) pe) => ir. apply /Zo_P; split; first (apply/Zo_P => //; split => //). apply:bijective_if_same_finite_c_inj; rewrite ? p2 ? p3 //. move => t tK; rewrite (restriction2_V pe tK); apply: qe; fprops. move => u v ug3 vg3; move: (pd _ ug3) (pd _ vg3) => pe pe' sr. move: ug3 => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [] /functionsP [qa qb qc] qd qe qf qg. move: vg3 => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P [] /functionsP [qa' qb' qc'] qd' qe' qf' qg'. apply: function_exten; rewrite ? qb' ? qc' //. rewrite qb -pa => t; case /setU1_P ; last by move => ->; rewrite qf. move => ti; case: (equal_or_not t x); first by move => ->; rewrite qg. move => tx; move /setC1_P: (conj ti tx) => tK. by rewrite - (restriction2_V pe tK) - (restriction2_V pe' tK) sr. move => y ydK. move: ydK => /Zo_P [] /Zo_P [] /functionsP [fy sy ty] biy nfy. pose f z := Yo (z = csucc n) x (Yo (z = x) (csucc n) (Vf y z)). have f1: f (csucc n) = x by rewrite /f; Ytac0; Ytac0. have f2: f x = (csucc n) by rewrite /f; Ytac0; Ytac0. have f3: forall t, inc t K -> f t = Vf y t. move => t /setC1_P [ti tk]; rewrite /f; Ytac0; Ytac h => //; case: pb; ue. have f4: forall t, inc t K -> inc (f t) K. move => t tk; rewrite (f3 _ tk); rewrite - ty; Wtac. have f5: lf_axiom f I' I'. move => t; rewrite -pa; case: (equal_or_not t x). by move ->; rewrite f2; fprops. move => tx; case/setU1_P => ta; last by rewrite ta f1; fprops. by rewrite pa; apply: ski'; apply: f4;apply /setC1_P. have f6: function (Lf f I' I') by apply:lf_function. have f7: restriction2_axioms (Lf f I' I') K K. have h: sub K (source (Lf f I' I')) by aw. red; aw;split => // t; move /(Vf_image_P f6 h) => [u uK]. by rewrite LfV//; fprops => ->; apply: f4. move: (restriction2_prop f7) => [p1 p2 p3]. have f8: (restriction2 (Lf f I' I') K K) = y. apply: function_exten; rewrite ? p2 ? p3 //. move => t tk /=; rewrite (restriction2_V f7) // LfV//; fprops. have f9: forall t, inc t I' -> f t <> t. move => t; rewrite -pa; case: (equal_or_not t x). move => -> _; rewrite f2 //. move => tx; case /setU1_P; last by move => ->; rewrite f1; fprops. move => ti; move /setC1_P: (conj ti tx) => tK. by rewrite (f3 _ tK);apply: nfy. have f10: inc (Lf f I' I') (permutations I'). apply /Zo_P; split; first by apply /functionsP; red;saw. apply:bijective_if_same_finite_c_surj; aw; trivial. apply /lf_surjective => //. move => z; rewrite - pa; case /setU1_P; last first. move => ->; exists x;fprops. case: (equal_or_not z x)=> zx zi. by rewrite zx; exists (csucc n); fprops. move /setC1_P: (conj zi zx); rewrite -/K - ty => yt. move: (bij_surj biy yt) => [w]; rewrite sy => wK ->. by rewrite - (f3 _ wK); exists w=> //; rewrite pa; apply: ski'. exists (Lf f I' I')=> //; apply /Zo_P; rewrite LfV// ; split => //. apply /Zo_P; rewrite ! LfV//;split => //. by apply /Zo_P;split => // => t ti; rewrite LfV//; apply: f9. set G4 := Zo G2 (fun f => Vf f x <> csucc n). have ->: (G2 -s G3) = G4. set_extens t. by move /setC_P => [tg2] /Zo_P p3; apply /Zo_P;split => // h; case: p3. by move => /Zo_P [p1 p2]; apply /setC_P;split => // ; move => /Zo_P [q1 q2]. pose g f := fun z => Yo (z = Vf (inverse_fun f) (csucc n)) x (Vf f z). pose g1 f := Lf (g f) I I. have pd: forall f (y:= Vf (inverse_fun f) (csucc n)), inc f G4 -> [/\ Vf f y = csucc n, inc y I, (g f y) = x, (forall t, t <> y -> (g f t) = Vf f t) & (forall z, inc z I -> inc (g f z) I)]. move => f y /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P []. move /functionsP => [ff sg tf] bf nfp fn fx. move:(inverse_bij_fb bf) => ifb. have stf: inc (csucc n) (target f) by rewrite tf -pa; fprops. have ysf: inc y (source f). by move: (Vf_target (proj1 (proj1 ifb))); aw; apply. have f1: Vf f y = csucc n by rewrite /y inverse_V //. have yI: inc y I. rewrite sg in ysf; move: (nfp _ ysf) => yy. by move: ysf; rewrite -pa; case /setU1_P => // ysn; case: yy; rewrite f1. have f2: x <> y by dneg w; ue. have f3: (g f y) = x by rewrite /g /y; Ytac0. have f4: forall t, t <> y -> (g f t) = Vf f t. by move => t; rewrite /y /g => ty; Ytac0. have f5: (forall z, inc z I -> inc (g f z) I). move => z zI; case: (equal_or_not z y); first by move => ->; rewrite f3. move => zy; rewrite (f4 _ zy). have zsi: inc z (source f) by rewrite sg -pa; fprops. move: (Vf_target ff zsi); rewrite tf - pa; case /setU1_P => //. by move => h; rewrite -h in f1; case: zy; rewrite (bij_inj bf ysf zsi f1). done. have fsi: finite_set I by red; rewrite ci; apply /NatP. move: (nbder_pr fsi); rewrite ci => <-. apply /card_eqP; exists (Lf g1 G4 (derangements I)). saw; apply: lf_bijective. move => f fg4; move: (pd _ fg4). set y := (Vf (inverse_fun f) (csucc n)); move=> [f1 yI f3 f4 f5]. move: fg4 => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P []. move /functionsP => [ff sg tf] bf nfp fn fx. have f2: x <> y by dneg w; ue. have f6: function (g1 f) by apply /lf_function. have f7: bijection (g1 f). rewrite /g1. apply:bijective_if_same_finite_c_surj; aw; trivial. apply /lf_surjective => //. move => t tI; have ti': inc t (target f) by rewrite tf -pa; fprops. move: (bij_surj bf ti'); rewrite sg; move => [u ui uv]. rewrite -pa in ui;case /setU1_P: ui; last first. move => h; exists y => //; rewrite f3 uv h fn => //. by move => ui; ex_tac; rewrite f4 // => uy; case: pb; rewrite -f1 - uy -uv. have f8: inc (g1 f) (permutations I). by apply /Zo_P;split => //; rewrite /g1;apply /functionsP;red;aw. apply /Zo_P; split => // t ti; case: (equal_or_not t y). by move => ty; rewrite /g1 LfV// ty f3. move => ty; rewrite /g1 LfV//; rewrite (f4 _ ty). apply: nfp; rewrite -pa; fprops. move => u v ug4 vg4 sg1. move: (ug4) => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P []. move /functionsP => [ff sg tf] bf nfp fn fx. move: (vg4) => /Zo_P [] /Zo_P [] /Zo_P [] /Zo_P []. move /functionsP => [ff' sg' tf'] bf' nfp' fn' fx'. apply: function_exten; rewrite ? sg ?sg' ? tf' //. move => t; rewrite - pa; case /setU1_P; last by move => ->; rewrite fn fn'. move => tI. move: (pd _ ug4) (pd _ vg4). set y := (Vf (inverse_fun u) (csucc n)); move=> [f1 yI f3 f4 f5]. set y' := (Vf (inverse_fun v) (csucc n)); move=> [f1' yI' f3' f4' f5']. move: (f_equal (fun z => Vf z t) sg1); rewrite /g1 ! LfV//. have tsn: t <> csucc n by move => h; case: pb; rewrite -h. have i1: Vf v (csucc n) <> Vf v t. have tsv: inc t (source v) by rewrite sg' - pa; fprops. have nsv: inc (csucc n) (source v) by rewrite sg' - pa; fprops. by move => h; case: tsn; rewrite (bij_inj bf' nsv tsv h). have i2: Vf u (csucc n) <> Vf u t. have tsv: inc t (source u) by rewrite sg - pa; fprops. have nsv: inc (csucc n) (source u) by rewrite sg - pa; fprops. by move => h; case: tsn; rewrite (bij_inj bf nsv tsv h). case: (equal_or_not t y) => ty. rewrite {1 3} ty f3 f1. case: (equal_or_not t y'); first by move => ->; rewrite f1'. by move => ty'; rewrite (f4' _ ty') - fn'. rewrite (f4 _ ty); case: (equal_or_not t y') => ty'; last by rewrite f4'. rewrite ty' f3' f1' - fn - ty' => h; by case: i2. move => y /Zo_P [] /Zo_P [] /functionsP [fy sy ty] biy dy. set xx := Vf (inverse_fun y) x. move:(inverse_bij_fb biy) => iyb. have xty: inc x (target y) by ue. have xxsf: inc xx (source y). by move: (Vf_target (proj1 (proj1 iyb))); aw; rewrite ty; apply. have xxns: xx <> csucc n by move => h; case: pb; rewrite -h - sy. have f1: Vf y xx = x by rewrite /xx inverse_V //. pose f z := Yo (z = csucc n) x (Yo (z = xx) (csucc n) (Vf y z)). have f2: f (csucc n) = x by rewrite /f; Ytac0; Ytac0. have f3: f xx = (csucc n) by rewrite /f; Ytac0; Ytac0. have f4: forall t, t <> csucc n -> t <> xx -> f t = Vf y t. by move => t t1 t2; rewrite /f; Ytac0; Ytac0. have f5: f x <> csucc n. rewrite /f; Ytac0; Ytac xa; first by case: (dy _ xK); rewrite xa f1. move => h; case: pb; rewrite -h - ty; Wtac. have f6: forall t, inc t I' -> inc (f t) I'. move => t; rewrite -pa => ti; case: (equal_or_not t (csucc n)) => tn. rewrite tn f2; fprops. case: (equal_or_not t xx) => txx. rewrite txx f3; fprops. rewrite (f4 _ tn txx); apply /setU1_P; left. rewrite -ty; Wtac; rewrite sy; case /setU1_P: ti => //. have f7: function (Lf f I' I') by apply /lf_function. have f8: bijection (Lf f I' I'). apply:bijective_if_same_finite_c_surj; aw; trivial. apply /lf_surjective => //. move => t; rewrite -pa => /setU1_P; case; last first. move => ->; exists xx=> //; rewrite - sy;fprops. rewrite - ty => tty; move: (bij_surj biy tty) => [a asy av]. have asn: a <> csucc n by move => h; case: pb; rewrite -h - sy. case: (equal_or_not a xx); last first. by move =>axx; rewrite ty - sy; exists a;fprops; rewrite av f4. by move => ax; exists (csucc n); fprops;rewrite f2 av ax f1. have f9: inc (Lf f I' I') G1. apply /Zo_P; split. by apply /Zo_P;split => //;apply /functionsP;red; aw. move => t ti;rewrite LfV //; case: (equal_or_not t (csucc n)) => tn; first by rewrite tn f2; fprops. case: (equal_or_not t xx) => tx; first by rewrite tx f3; fprops. by rewrite (f4 _ tn tx); apply: dy; move: ti; rewrite -pa; case /setU1_P. have f10: inc (Lf f I' I') G4 by apply:Zo_i;try apply:Zo_i => //; rewrite LfV. have II: sub I I' by rewrite -pa => t ti; fprops. have f11: Vf (inverse_fun (Lf f I' I')) (csucc n) = xx. have xxI': inc xx I' by apply: II; rewrite - sy. have ->: csucc n = Vf (Lf f I' I') xx by rewrite LfV. by rewrite inverse_V2 //; aw. have f12: lf_axiom (g (Lf f I' I')) I I. move => t ti; move: (II _ ti) => ti'; rewrite /g LfV// f11. Ytac aux; fprops; rewrite - ty; rewrite (f4 _ _ aux); try Wtac. by move => tn; case: pb; rewrite -tn. have f13: function (Lf (g (Lf f I' I')) I I) by apply: lf_function. ex_tac; rewrite /g1; apply: function_exten; aw;trivial. rewrite sy => t ti; move: (II _ ti) => ti';rewrite /g LfV//. rewrite f11; Ytac aa ; rewrite ? aa // LfV// f4//. by move => tn; case: pb; rewrite -tn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)