proposition: Lemma Sperner_cf3 f C: free_rep f -> inc C Sperner_mx_chain -> chain_free_meet f C = \0c \/ exists i, [/\ inc i (source f), inc (Vf f i) C & chain_free_meet f C = (csucc i)].
proof: Proof. move => fp Cp. case: (p_or_not_p (forall i, inc i (source f) -> ~inc (Vf f i) C)) => h. left;exact:(Sperner_cf2 fp Cp h). have [i isf fii]: (exists2 i, inc i (source f) & inc (Vf f i) C). ex_middle bad; case: h => i ha hb; case bad; ex_tac. move: (Sperner_cf1 fp Cp isf fii) => aux. by right; exists i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)