proposition: Lemma Sperner_1 A B k: natp k -> cardinal A = k -> cardinal B = k -> sub A B -> A = B.
proof: Proof. move => kN cA cB sAB. apply: (extensionality sAB); apply:empty_setC. move: (cardinal_setC2 sAB); rewrite - csum2cl - csum2cr cA cB -{1}(Nsum0r kN). have nD: natp (cardinal (B -s A)). have s1: sub (B -s A) B by move => t /setC_P []. have fsj: finite_set B by apply/NatP; ue. apply /NatP; apply: (sub_finite_set s1 fsj). by move/ (csum_eq2l kN NS0 nD); move /esym /card_nonempty. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)