proposition: Lemma Sperner_7 C: inc C Sperner_mx_chain -> lf_axiom cardinal C (csucc n) /\ bijection (Lf cardinal C (csucc n)).
proof: Proof. move => /Zo_P[ha hb]. move: (Sperner_3 ha) => hc. move:(subp_osr E) Sperner_p0 => [or sr] nN. move:ha=> /total_subordersP [qa qb]. have aux A: inc A C -> cardinal A <=c n. by rewrite sr in qa; move/qa => /setP_P /sub_smaller. have ax: lf_axiom cardinal C (csucc n) by move => t /aux /(NleP nN). split => //;apply: bijective_if_same_finite_c_inj; aw. - by rewrite hb (card_nat (NS_succ nN)). - apply /NatP; rewrite hb; fprops. - by apply: lf_injective. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)