proposition: Lemma Sperner_cf15 f (F := fun k => (subsets_with_p_elements k E)): free_rep f -> source f = cn -> exists k, [/\ natp k, is_half_n n k & target f = F k].
proof: Proof. move => ha hb. have nN:= Sperner_p0. move: (NS_half nN) => hN; move: (NS_succ hN) => shN. have: is_half_n n (chalf n) by left. case: (p_or_not_p (evenp n)) => en. by exists (chalf n); rewrite (Sperner_cf13 ha hb en). have on: oddp n by []. case:(Sperner_cf14 ha hb on) => ->; first by exists (chalf n). exists (csucc (chalf n)); split => //. right; rewrite {1} (half_odd on) /cdouble - csum_nn - (csum_nS _ hN). by apply: (cdiff_pr1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)