proposition: Lemma Sperner_p2 k: k <=c n -> cardinal (subsets_with_p_elements k E) = binom n k.
proof: Proof. move: Sperner_p0 => nN h; move: (NS_le_nat h nN) => kN. by rewrite - (card_p_subsets nN kN (erefl n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)