proposition: Lemma Sperner_19 A (k := cardinal A): sub A E -> cardinal (Zo Sperner_mx_chain (inc A)) = factorial k *c (factorial (n -c k)).
proof: Proof. move => sAE. rewrite -(Sperner_18 sAE). pose F g := fun_image (csucc n) (Vfs g). move: (sub_smaller sAE); rewrite -/k -/n => lekn. have nN:= Sperner_p0. have kN := (NS_le_nat lekn nN). set W := Zo _ _; set V := Zo _ _; suff: bijection (Lf chain_of_fun V W). by move/card_bijection; aw. apply: lf_bijective. - move => g /Zo_P [/bijectionsP bgp gc]. move:(Sperner_5 bgp) => h. by apply/Zo_P; split => //; apply/funI_P; exists k => //; apply/NleP. - by move => u v /Zo_S/bijectionsP uu /Zo_S/bijectionsP vv; apply:Sperner_13. - move => t /Zo_P [/Sperner_10] [ bgp ->] /funI_P [i lin Ai]. set g:= Lf _ _ _. have axa: k = i. move/(NleP nN): lin bgp=> [ci _ ssin] [[qa _] sg tg]. by rewrite /k Ai cardinal_image ? sg // (card_card ci). by exists g => //; apply/Zo_P; split; [ apply/bijectionsP | ue ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)