proposition: Lemma Sperner_3 C: inc C (total_suborders r) -> {inc C &, injective cardinal}.
proof: Proof. move => /total_subordersP [qa qb] A B AC BC /= sc. move:(subp_osr E) Sperner_p0 => [or sr] nN. have kN: natp (cardinal A). by apply /(NS_le_nat _ nN) /sub_smaller /setP_P; rewrite - sr;apply: qa. move: (proj2 qb A B); rewrite iorder_sr// => h; case: (h AC BC) => /iorder_gle1 /sub_gleP. by move/proj33 => sAB; apply:(Sperner_1 kN _ _ sAB). by move/proj33 => sAB; symmetry;apply:(Sperner_1 kN _ _ sAB). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)