proposition: Lemma Sperner_16 U: sub U E -> exists2 g, bijection_prop g n E & Vfs g (cardinal U) = U.
proof: Proof. move => suE; set V := (E -s U). have svE: sub V E. by move => t /setC_P []. have fsU: natp(cardinal U). apply/card_finite_setP;exact: (sub_finite_set suE fsE). have fsV: natp(cardinal V). apply/card_finite_setP;exact: (sub_finite_set svE fsE). move: (Sperner_15 fsU fsV (set_I2Cr E U)). by rewrite (setU2_Cr suE) /n (cardinal_setC2 suE) csum2cl csum2cr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)