proposition: Lemma Sperner_cf11 f : free_rep f -> (source f) = cn -> (forall C, inc C Sperner_mx_chain -> exists2 i, inc i (source f) & inc (Vf f i) C) /\ (forall i, inc i (source f) -> is_half_n n (cardinal (Vf f i))).
proof: Proof. move => fp cs. have nN := Sperner_p0. move: (Sperner_cf5 fp)(Sperner_cf8 fp). set c1 := (cn *c cardinal _); set c := csumb _ _ => eq1 [cN le1 hp]. have ncN: natp cn by apply: (NS_binom nN (NS_half _)). have cc: cardinalp c by apply: CS_nat. have cc1: cardinalp c1 by apply: CS_prod2. have sN: natp (c1 +c c) by rewrite - eq1;apply:(NS_prod ncN (NS_factorial nN)). have c1N:=(NS_in_suml cc1 sN). rewrite csumC in eq1. move: (csum2_compare_spec cN c1N eq1) => [qa qb]. have c1z : c1 = \0c. by apply:qb; apply:cleA => //; move: le1; rewrite cs eq1. have cnz: cn <> \0c by apply: (binom_pr3 nN (NS_half nN) (cle_halfn_n nN)). split. move => C Cp. case: (cprod2_eq0 c1z) => // /card_nonempty xfmz. case: (Sperner_cf3 fp Cp) => cp; first by empty_tac1 C; apply/Zo_P. move:cp => [i [isf iv _]]; ex_tac. have /hp T: source f *c factorial n = c by rewrite cs eq1 c1z (csum0r cc). move=> i ip; move: (T i ip). rewrite (proj2 (Sperner_cf7 fp ip)) => /esym av. have /sub_smaller lan: sub (Vf f i) E. move:fp =>[ qe _ /Sperner_p4/proj1 qc]. by move /setP_P: (qc _ (Vf_target (proj1(proj1 qe)) ip)). exact: (Sperner_b2 nN lan av). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)