proposition: Lemma Sperner_11 w i (C := chain_of_fun w) (F := Vf (inverse_fun (Lf cardinal C (csucc n)))): bijection_prop w n E -> i <=c n -> Vfs w i = F i.
proof: Proof. move => wp lin. move: (Sperner_5 wp) Sperner_p0 => CC nN. have ci: cardinal i = i by apply: (card_card (proj31 lin)). move: (Sperner_7 CC) => [Ha Hb]. move: (wp) => [[iw _] sw tw]. have siw: sub i (source w) by rewrite sw; apply: (proj33 lin). have qa: inc (Vfs w i) C by apply/funI_P; exists i => //; apply /NleP. have qb: cardinal (Vfs w i) = i by rewrite (cardinal_image siw iw). by rewrite - (inverse_V2 Hb (y := Vfs w i)) // -/F; aw;bw => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)