proposition: Lemma Sperner_cf13 f (F := (subsets_with_p_elements (chalf n) E)): free_rep f -> source f = cn -> evenp n -> target f = F.
proof: Proof. move :Sperner_p0 => nN fp sg en. move: (proj2(Sperner_cf11 fp sg)) => H. have aux: is_half_n n (chalf n)by left. apply: (Sperner_cf12 fp sg (cle_halfn_n nN) aux). move: (fp) => [[injp [_ sj]] cf /Sperner_p4/proj1 ste]. move => i itf; apply /Zo_P; split; first by move: (ste _ itf). move: (sj _ itf) =>[k kf ->];case: (H _ kf) => // dv. move: (Sperner_cf0 fp kf) =>[_ q1 q2]. move: (cdiff_pr q1); rewrite dv {2} (half_even en) /cdouble - csum_nn. apply:(csum_eq2r (NS_half nN) q2 (NS_half nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)