proposition: Lemma Sperner_p5 k: k <=c n -> inc (subsets_with_p_elements k E) (free_subsets r).
proof: Proof. by move =>h; apply/Sperner_p4; split;[ apply: Zo_S | apply:Sperner_p1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)