proposition: Lemma Sperner_13 w1 w2: bijection_prop w1 n E -> bijection_prop w2 n E -> chain_of_fun w1= chain_of_fun w2 -> w1 = w2.
proof: Proof. move => p1 p2 sv. move:Sperner_p0 => nN. move:(p1)(p2) => [qa qb qc][qd qe qf]. apply: function_exten; try fct_tac; try ue; rewrite qb => i iin. move/(NltP nN): (iin) => lin. have lein: csucc i <=c n by apply/(cleSlt0P (proj31_1 lin) nN). rewrite (Sperner_12 p1 lin) (Sperner_12 p2 lin). rewrite (Sperner_11 p1 lein) (Sperner_11 p2 lein) (Sperner_11 p2 (proj1 lin)). by rewrite (Sperner_11 p1 (proj1 lin)) sv. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)