proposition: Lemma Sperner_14: cardinal Sperner_mx_chain = factorial n.
proof: Proof. have: n \Eq E by apply/card_eqP; rewrite /n double_cardinal. move/ (equipotent_ex_pr); set f := (equipotent_ex n E) => fp. move:Sperner_p0 => nN. pose phi g:= chain_of_fun (f \co g). suff: bijection (Lf phi (permutations n) Sperner_mx_chain). have fse: finite_set n by apply: finite_set_nat. move/card_bijection; aw => <-. by rewrite card_permutations // /n double_cardinal. have ax: lf_axiom phi (permutations n) Sperner_mx_chain. by move => t /permutationsP bpt; move: (compose_bp bpt fp) => /Sperner_5. move: (inverse_bij_bp fp)=> fip. apply: (lf_bijective ax); last first. move => C hc; move: (Sperner_10 hc)=> []; set g := Lf _ _ _ => gp ->. move: (compose_bp gp fip) => cb. exists ((inverse_fun f) \co g); first by apply/permutationsP. move: fp gp => [Ha _ Hb] [[[Hc _] _] _ Hd ]. rewrite /phi compf_lK' //; ue. move => u v /permutationsP up /permutationsP vp. move: (compose_bp up fp) (compose_bp vp fp); rewrite /phi => b1 b2 sv. have: (f \co u) = (f \co v) by apply:Sperner_13. move: fp up vp =>[bf sf _] [[[fu _] _] _ tu] [[[fv _] _] _ tv]. move: (proj1 (proj1 bf))=> ff; apply:(compf_regr bf); split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)