proposition: Lemma Sperner_8 C (F := Vf (inverse_fun (Lf cardinal C (csucc n)))): inc C Sperner_mx_chain -> forall i, i <=c n -> inc (F i) C /\ cardinal (F i) = i.
proof: Proof. move:Sperner_p0 => nN /Sperner_7 [ax card_b] i lin. have itg: inc i (target (Lf cardinal C (csucc n))) by aw; apply/(NleP nN). move: (inverse_Vis card_b itg);aw => ifC; split => //. move: (inverse_V card_b itg); rewrite LfV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)