proposition: Lemma Sperner_cf9 f : free_rep f -> (source f) <=c cn.
proof: Proof. move => fp. move: (Sperner_cf5 fp)(Sperner_cf8 fp). set c1 := (cn *c cardinal _); set c := csumb _ _ => eq1 /proj32 le1. have cc: cardinalp c by rewrite /c/csumb/ csum; fprops. have nN := Sperner_p0. move: (cleT le1 (csum_Mle0 c1 cc)); rewrite - eq1 => h. have ncN: natp cn by apply: (NS_binom nN (NS_half _)). exact:(cprod_le2r (NS_factorial nN) (proj32 fp) ncN (factorial_nz nN) h). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)