proposition: Lemma nbder_pr E: finite_set E -> cardinal (derangements E) = nbder (cardinal E).
proof: Proof. have aux: forall I J g f, bijection g -> source g = J -> target g = I -> inc f (derangements J) -> inc (g \co (f \co inverse_fun g)) (derangements I). move => I J g f big sg tg. move: (inverse_bij_fb big); set g1 := inverse_fun g => igb. move: (proj1 (proj1 big))(proj1(proj1 igb)) => fg fig. move => /Zo_P [] /Zo_P [] /functionsP [pa pb pc] pd pe. have qa: (f \coP g1) by rewrite /g1;red; saw; ue. have qb: bijection (f \co g1) by apply: compose_fb. have qc: (g \coP (f \co g1)) by saw; try fct_tac; ue. have qd: bijection (g \co (f \co g1)) by apply: compose_fb. have sg1: source g1 = I by rewrite /g1; aw. have qe: inc (g \co (f \co g1)) (permutations I). apply /Zo_P;split => //; apply /functionsP; saw;fct_tac. apply/ Zo_P; split => // => x xi /(f_equal (Vf g1)). rewrite - sg1 in xi; bw; aw => //; rewrite -/g1; set y:= Vf g1 x. have ye: inc y J by rewrite- sg - ifun_t /y /g1; Wtac; aw. have ysg: inc (Vf f y) (source g) by rewrite sg - pc; Wtac. rewrite (inverse_V2 big ysg); exact (pe _ ye). move => fse; set n := cardinal E; set I := Nint n. have nN: natp n by apply /NatP. have : n = cardinal I by rewrite (card_Nint nN). move/card_eqP => [g [big sg tg]]; apply /card_eqP. pose c f := g \co (f \co (inverse_fun g)). move: (inverse_bij_fb big); set g1 := inverse_fun g => igb. move: (proj1 (proj1 big))(proj1(proj1 igb)) => fg fig. exists (Lf c (derangements E) (derangements I)); saw. apply: lf_bijective. by move => f;apply: aux. move => u v /Zo_P [] /Zo_P [] /functionsP [pa pb pc] _ _. move => /Zo_P [] /Zo_P [] /functionsP [qa qb qc] _ _ sv. have ra: (u \coP g1) by rewrite /g1;red; saw; ue. have rb: function (u \co g1) by fct_tac. have rc: (g \coP (u \co g1)) by saw; ue. have ra': (v \coP g1) by rewrite /g1;red; saw; ue. have rb': function (v \co g1) by fct_tac. have rc': (g \coP (v \co g1)) by saw; ue. move: (fct_co_simpl_left rc rc' big sv) => sv1. exact: (fct_co_simpl_right ra ra' igb sv1). move => y yv; set x := (g1 \co (y \co (inverse_fun g1))). have sg1: source g1 = I by rewrite /g1; aw. have tg1: target g1 = E by rewrite /g1; aw. move: (aux _ _ _ _ igb sg1 tg1 yv); rewrite (ifun_involutive fg) => h; ex_tac. move: yv => /Zo_P [] /Zo_P [] /functionsP [fy sy ty] _ _. rewrite /c -/g1. have pa: (y \coP g) by split => //; ue. have pb: function (y \co g) by fct_tac. have pc: g1 \coP (y \co g) by saw; ue. have pd: (y \co g) \coP g1 by saw; ue. have pe: g1 \coP ((y \co g) \co g1) by red;aw;split => //; try fct_tac; ue. move: (composable_f_inv big) => pf. rewrite - compfA // compfA // bij_right_inverse //. rewrite - compfA // bij_right_inverse // tg - {2} sy compf_id_r //. rewrite - ty compf_id_l //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)