proposition: Lemma Sperner_b1 n k: natp n -> k <=c n -> (factorial n) <=c (binom n (chalf n)) *c ((factorial k) *c (factorial (n -c k))).
proof: Proof. move => nN lkn. move:(NS_le_nat lkn nN) => kN. rewrite - (binom_good nN kN lkn). by apply: cprod_Mleeq; apply: binom_max. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)