proposition: Lemma Sperner_b2 n k: natp n -> k <=c n -> (factorial n) = (binom n (chalf n)) *c ((factorial k) *c (factorial (n -c k))) -> is_half_n n k.
proof: Proof. move => nN lkn. move:(NS_le_nat lkn nN)(NS_diff k nN) => kN dN h. apply/(binom_monotone_max_arg nN lkn). move: h; rewrite - (binom_good nN kN lkn) ; apply: cprod_eq2r. - by apply:NS_prod; apply: NS_factorial. - by apply: NS_binom. - by apply: (NS_binom nN (NS_half nN)). - by apply: cprod2_nz; apply: factorial_nz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)