proposition: Lemma Sperner_2 E k (F := subsets_with_p_elements k E): natp k -> free_subset (subp_order E) F.
proof: Proof. move => kN i j /Zo_P [/setP_P iE ci] /Zo_P[ /setP_P jE cj]. move/ sub_gleP => [_ _ sij]; apply: (Sperner_1 kN ci cj sij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)