proposition: Lemma Sperner_cf0 f i: free_rep f -> inc i (source f) -> [/\ sub (Vf f i) E, cardinal (Vf f i) <=c n & natp (cardinal (Vf f i))].
proof: Proof. move: Sperner_p0 => nN fp isf. have sE: sub (Vf f i) E. move:fp =>[ qa qb /Sperner_p4/proj1 qc]. by move /setP_P: (qc _ (Vf_target (proj1(proj1 qa)) isf)). move: (sub_smaller sE) => le1. split => //; apply/(NS_le_nat le1 nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)