proposition: Lemma Sperner_21 : order_width r cn.
proof: Proof. split; last exact: Sperner_20. move: Sperner_p0 => nN. move: (cle_halfn_n nN) => lehn. move: (Sperner_p2 lehn) (Sperner_p5 lehn) => p1 p2. ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)