proposition: Lemma Sperner_4 C: inc C (total_suborders r) -> cardinal C <=c (csucc n).
proof: Proof. move =>h; move: (Sperner_3 h) => ci. move:h=> /total_subordersP [qa qb]. move:(subp_osr E) Sperner_p0 => [or sr] nN. have aux A: inc A C -> cardinal A <=c n. by rewrite sr in qa; move/qa => /setP_P /sub_smaller. rewrite - (cardinal_fun_image ci) - (card_Nintc nN). by apply: sub_smaller => t /funI_P [A /aux c ->]; apply/(NintcP nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)