proposition: Lemma Sperner_20 A: inc A (free_subsets r) -> cardinal A <=c cn.
proof: Proof. move / free_rep_prop1 => [f fp <-]; move: (Sperner_cf9 fp) => le1. by rewrite - (card_bijection (proj31 fp)) (card_nat (proj32 fp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)