proposition: Lemma Sperner_12 w i: bijection_prop w n E -> i <c n -> (Vf w i) = union (Vfs w (csucc i) -s Vfs w i).
proof: Proof. move => [[iw [fw _]] sw tw] lin. move:Sperner_p0 => nN. move: (NS_lt_nat lin nN) => iN. set A := Vfs w (csucc i); set B := Vfs w i. suff: A -s B = singleton (Vf w i) by move ->; rewrite setU_1. have lsin: csucc i <=c n by apply/(cleSltP iN). have sisw: sub (csucc i) (source w) by rewrite sw; exact: (proj33 lsin). have isw: sub i (source w) by rewrite sw; exact: (proj33 (proj1 lin)). apply: set1_pr. apply/setC_P; split. by apply/(Vf_image_P fw sisw); exists i => //; apply: Nsucc_i. have iisw: inc i (source w) by rewrite sw; apply/NltP. move/(Vf_image_P fw isw) => [j uj sva]. move: (proj2 iw i j iisw (isw _ uj) sva) => ij. by move: (ordinal_decent OS_omega iN); rewrite {1} ij; case. move => t /setC_P [/(Vf_image_P fw sisw) [j jsi ->] h]. move/(NleP iN): jsi; case/ cle_eqVlt; [by move -> | move => lij; case: h]. by apply /(Vf_image_P fw isw); exists j => //; apply/NltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)