proposition: Lemma card_injections E F: finite_set E -> finite_set F -> cardinal (injections E F) = (cardinal F) ^_c (cardinal E).
proof: Proof. move=> fse fsF. set (n:= cardinal F). have nN: natp n by apply /NatP. move: E fse (fse); apply: finite_set_induction0. rewrite cardinal_set0 ffactn0 => _. set f:= empty_function_tg F. suff ->: (injections emptyset F = singleton f) by rewrite cardinal_set1. move: (empty_function_tg_function F) => [pa pb pc]. have aux: inc f (functions emptyset F) by apply/functionsP. have injf: injection f by split => //; rewrite /f pb => x y; case; case. have ff: inc f (injections emptyset F) by apply/injectionsP. apply: set1_pr => // z /Zo_S vs; exact: (fun_set_small_source vs aux). move=> E a sE naE h. move: (sub_finite_set (@sub_setU1 E a) h) => fse. move/NatP: (fse);set (m := cardinal E) => mN. rewrite (csucc_pr naE) (ffactnSr _ mN) -(sE fse); clear sE h. set (G2:= injections (E +s1 a) F). set (G1:= injections E F). set rf:=Lf (restriction ^~ E) G2 G1. have <-: (source rf = G2) by rewrite /rf; aw. have <-: (target rf = G1) by rewrite /rf; aw. have ta: lf_axiom (restriction ^~ E) G2 G1. move=> t /injectionsP [[ft it] st tt]. have sat: sub E (source t) by rewrite st; fprops. move: (restriction_prop ft sat) => pp; move: (pp) => [pa pb pc]. apply/injectionsP; split => //; [ split => // x y; rewrite pb => xE yE| ue]. by rewrite restriction_V // restriction_V //; apply: it; apply:sat. have fr: function rf by apply: lf_function. apply: (shepherd_principle fr) => x. set(K:= Vfi1 rf x). rewrite lf_target; move/injectionsP => [injx sxE txF]; move: (proj1 injx) => fx. have fst: finite_set (target x) by hnf;rewrite txF;fprops. move:(cardinal_complement_image injx fst). set (C:= F -s (Imf x)). rewrite sxE txF -/n -/m -/C => <-. have tav:(lf_axiom (Vf ^~ a) K C). move => z /iim_fun_P [u /set1_P uz h1]; move: (Vf_pr fr h1). move: (p1graph_source fr h1); rewrite /rf lf_source => tG2. rewrite LfV // => xx. move: tG2 => /injectionsP [[fz iz] sz tgz]. have asz: inc a (source z) by rewrite sz; fprops. apply /setC_P; split; first by rewrite -tgz;Wtac. move /(Imf_P fx) => [y ysx]. have Ez: sub E (source z) by rewrite sz; fprops. have yE: inc y E by ue. rewrite - uz xx (restriction_V fz Ez yE) => /(iz _ _ asz (Ez _ yE)). by move => ya; case: naE; rewrite ya. set (val:= Lf (Vf ^~ a) K C). have fv: function val by apply: lf_function. have sv: (source val = K) by rewrite /val; aw. have tv: (target val = C) by rewrite /val; aw. apply /card_eqP; exists val; split => //; apply: lf_bijective =>//. move=> u v /iim_fun_P [u' /set1_P usx Jg1]. move => /iim_fun_P [v' /set1_P vsx Jg2] sv1. have uG2:inc u G2 by move:(p1graph_source fr Jg1); rewrite /rf; aw. have vG2:inc v G2 by move:(p1graph_source fr Jg2); rewrite /rf; aw. move: (Vf_pr fr Jg1) (Vf_pr fr Jg2); rewrite /rf LfV //LfV //. move: uG2 => /injectionsP [[fu inju] su tu]. move: vG2 => /injectionsP [[fvv injvØ]svv tvv] sr1 sr2. apply: function_exten=>//; [ue | ue | rewrite su]. move=> t; case /setU1_P => tE; [ transitivity (Vf x t) | by rewrite tE]. rewrite - usx sr1 restriction_V //; rewrite su; fprops. rewrite - vsx sr2 restriction_V //; rewrite svv; fprops. move=> y /setC_P [yF nyi]. have nasc: ~ (inc a (source x)) by ue. set (f:= extension x a y). have ff: function f by rewrite /f; apply: extension_f=>//. have sf: source f = E +s1 a by rewrite /f /extension; aw; ue. have tf: target f = F by rewrite - (setU1_eq yF) - txF /f/extension; aw. have injf: injection f. split =>//; move=> u v;rewrite sf /f;case /setU1_P => xsf; case /setU1_P=>ysf. - rewrite !extension_Vf_in //; try ue; apply: (proj2 injx); ue. - rewrite - sxE in xsf. rewrite ysf extension_Vf_out // extension_Vf_in //. move=> eq; rewrite -eq in nyi; case: nyi. apply /(Imf_P fx); ex_tac; apply: W_pr3 =>//. - rewrite - sxE in ysf. rewrite xsf extension_Vf_out // extension_Vf_in //. move=> eq; rewrite eq in nyi; case: nyi. apply /(Imf_P fx);ex_tac; apply: W_pr3 =>//. - by rewrite xsf ysf. have rFE:(restriction f E = x). have se: sub E (source f) by rewrite sf; fprops. move: (restriction_prop ff se) => [pa pb pc]. apply: function_exten=>//; rewrite ? pb //. by rewrite pc tf txF. move=> u uE /=; rewrite restriction_V // /f extension_Vf_in//; ue. have fG2: inc f G2 by apply/injectionsP. have fi:inc f (Vfi1 rf x). apply /iim_fun_P;exists x;fprops. have <-: (Vf rf f = x) by rewrite /rf LfV. by apply: Vf_pr3=>//; rewrite /rf;aw. by ex_tac; rewrite /f extension_Vf_out. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)