proposition: Lemma Sperner_cf12 f k (F := (subsets_with_p_elements k E)): free_rep f -> (source f) = cn -> k <=c n -> is_half_n n k -> sub (target f) F -> target f = F.
proof: Proof. move:Sperner_p0 => nN fp csf lekn hn stf. have ncN: natp cn by apply: (NS_binom nN (NS_half _)). move: (fp) => [bf qa qb]. have cf: (cardinal F) = cn. by rewrite /F(Sperner_p2 lekn);move/ (binom_monotone_max_arg nN lekn): hn. have cc: target f =c F. by rewrite - (card_bijection bf) csf cf (card_card (CS_nat ncN)). have ha: finite_set F by apply/NatP; rewrite cf. exact: (cardinal_setC5 ha stf cc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)