proposition: Lemma Sperner_18 A (k := cardinal A): sub A E -> cardinal (Zo (bijections n E) (fun g => Vfs g k = A)) = factorial k *c (factorial (n -c k)).
proof: Proof. move => sAE. have kN: natp k by apply/NatP; apply: (sub_finite_set sAE fsE). have nN:= Sperner_p0. set B := (Zo (bijections n n) (fun g => Vfs g k = k)). set C := Zo _ _. have lekn: k <=c n by move: (sub_smaller sAE). have skn := proj33 lekn. have ck := proj31 lekn. move: (Sperner_16 sAE) => [g ga1 ga2]. have: bijection (Lf (compose g) B C). move: (ga1) =>[bg sg tg]. apply: lf_bijective. + move => f/Zo_P [/bijectionsP bf fp]. apply/Zo_P; split; last by rewrite compf_image fp. apply/bijectionsP; apply: (compose_bp bf ga1). + move => u v /Zo_P [/bijectionsP [bf sf tf] fp]. move => /Zo_P [/bijectionsP [bv sv tv] p]. apply/ (compf_regr bg); split => //; try fct_tac; ue. + move => f /Zo_P [/bijectionsP bf fp]. move:(inverse_bij_bp ga1)(proj1 bg) => ga3 ig. have aux: Vfs (inverse_fun g \co f) k = k. rewrite compf_image fp - ga2 inverse_direct_image_inj //. rewrite sg; apply: skn. move: (bf) =>[bif sf tf]. exists ((inverse_fun g) \co f). apply/Zo_P; split => //; apply/bijectionsP; apply: (compose_bp bf ga3). rewrite compf_lK' //; try fct_tac; ue. move/(card_bijection); aw => <-. clear C g ga1 ga2. have s1: sub (n -s k) n by move => t/setC_P []. have fsn: finite_set n by apply: finite_set_nat. have fsd := (sub_finite_set s1 fsn). pose phi1 f := restriction2 f k k. pose phi2 f := restriction2 f (n-s k) (n -s k). have rax1 f: inc f B -> restriction2_axioms f k k. rewrite /restriction2_axioms. by move => /Zo_P [/bijectionsP[/proj1/proj1 fs -> ->] ->]; split. have rax2 f: inc f B -> restriction2_axioms f (n -s k) (n -s k). rewrite /restriction2_axioms. move => /Zo_P [/bijectionsP[/proj1 [ ff injf] sf tf] Vfk]. have ha: sub (n -s k) (source f) by ue. have hb: sub k (source f) by ue. rewrite sf tf; split => // t /(Vf_image_P ff ha) [i lein ->]; apply/setC_P. have hc: inc (Vf f i) n by Wtac. split => //; rewrite - Vfk => /(Vf_image_P ff hb) [u uk ]. move /(injf i u (ha _ lein) (hb _ uk)) => iu. move/setC_P: lein => /proj2; case; ue. have perm_phi1 f: inc f B -> inc (phi1 f) (permutations k). move => fB; move:(rax1 f fB) => ax. move: (restriction2_prop ax) => rp2; move: (rp2) =>[fg sg tg]. move: fB =>/Zo_P [/bijectionsP[ [qa qb] _ _ ] _]. apply:(permutation_if_inj (finite_set_nat kN) rp2). apply: (restriction2_fi qa ax). have perm_phi2 f: inc f B -> inc (phi2 f) (permutations (n -s k)). move => fB; move:(rax2 f fB) => ax. move: fB =>/Zo_P [/bijectionsP[ [qa qb] _ _ ] _]. move: (restriction2_prop ax) => rp2; move: (rp2) =>[fg sg tg]. apply:(permutation_if_inj fsd rp2); apply: (restriction2_fi qa ax). pose phi3 f := J (phi1 f) (phi2 f). suff: (bijection (Lf phi3 B ((permutations k) \times (permutations (n -s k))))). move/card_bijection; aw; rewrite - cprod2_pr1 - cprod2cl - cprod2cr. have fsk: finite_set k by apply: finite_set_nat. by rewrite (card_permutations fsk)(card_permutations fsd) (card_card ck). apply: lf_bijective. + by move => t tB; apply: setXp_i; [ apply:perm_phi1 | apply:perm_phi2]. + move => u v uB vB sphi; move: (pr1_def sphi) (pr2_def sphi) => eq1 eq2. move/Zo_P: (uB) => [ /bijectionsP [[[fu _] _] su tu] uk ]. move/Zo_P: (vB) => [ /bijectionsP [[[fv _] _] sv tv] vk ]. apply: function_exten => //; try ue; rewrite su => t itn. case: (inc_or_not t k) => tk. move: (rax1 _ uB) (rax1 _ vB) => a1 a2. move: (f_equal (Vf ^~ t) eq1). by rewrite (restriction2_V a1 tk)(restriction2_V a2 tk). move: (rax2 _ uB) (rax2 _ vB) => a1 a2. have tnk: inc t (n -s k) by apply/setC_P. move: (f_equal (Vf ^~ t) eq2). by rewrite (restriction2_V a1 tnk)(restriction2_V a2 tnk). + move => y /setX_P [py /permutationsP [ba sa ta] /permutationsP [bb sb tb]]. pose c i := Yo (inc i k) (Vf (P y) i) (Vf (Q y) i). move: (proj1(proj1 ba))(proj1(proj1 bb)) => fa fb. move: (Vf_target fa); rewrite sa ta => hsa. move: (Vf_target fb); rewrite sb tb => hsb. have axc: lf_axiom c n n. rewrite /c;move => i iin /=; Ytac lik; first by apply: skn; Wtac. apply: s1; Wtac; rewrite sb;fprops. have ci: injection (Lf c n n). apply: (lf_injective axc) => i j iin jin. rewrite /c; Ytac lik; Ytac ljk. + by move: (proj2 (proj1 ba) i j); rewrite sa; apply. + move => eq. have: inc j (n -s k) by apply/setC_P. move/ hsb => /setC_P[_]; case; rewrite - eq; exact: (hsa i lik). + move => eq. have: inc i (n -s k) by apply/setC_P. move/ hsb => /setC_P[_]; case; rewrite eq; exact: (hsa j ljk). + by move: (proj2 (proj1 bb) i j); rewrite sb; apply; apply/setC_P. have fci := proj1 ci. have fpi: function_prop (Lf c n n) n n by saw. have bbcs: inc (Lf c n n) (bijections n n). apply:(permutation_if_inj (finite_set_nat nN) fpi ci). have aux i: inc i k -> Vf (P y) i = Vf (Lf c n n) i. by move => ik;move:(skn _ ik) => sin; rewrite LfV// /c; Ytac0. have ra: Vfs (Lf c n n) k = k. have qa: sub k (source (Lf c n n)) by aw. set_extens t. move/(Vf_image_P fci qa) => [u uk]; move: (skn _ uk) => un. rewrite LfV//; move ->; rewrite /c; Ytac0; Wtac. move => tk; apply/(Vf_image_P fci qa). have tim: inc t (target (P y)) by ue. move: ((proj2 (proj2 ba)) _ tim); rewrite sa; move => [i ik ->]; ex_tac. have cB :inc (Lf c n n) B by apply/Zo_P. have pp1: P y = phi1 (Lf c n n). move: (perm_phi1 _ cB)(rax1 _ cB) => /permutationsP [[[fc _] _] sc tc] ax. apply: function_exten=> //; try ue; rewrite sa => i ik. by rewrite /phi1 restriction2_V //; apply: aux. have pp2: Q y = phi2 (Lf c n n). move: (perm_phi2 _ cB)(rax2 _ cB) => /permutationsP [[[fc _] _] sc tc] ax. apply: function_exten=> //; try ue; rewrite sb => i ik. rewrite /phi1 restriction2_V //; move/setC_P: ik =>[qa qb]. by rewrite LfV///c; Ytac0. exists (Lf c n n); first by apply/Zo_P; split. rewrite/phi3;apply: pair_exten; aww. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)