proposition: Lemma Sperner_cf2 f C: free_rep f -> inc C Sperner_mx_chain -> (forall i, inc i (source f) -> ~inc (Vf f i) C) -> chain_free_meet f C = \0c.
proof: Proof. move => [[[ff fi] _] sfN rrf] hb hc. rewrite /chain_free_meet; set T := Zo _ _. suff: T = emptyset by move ->; rewrite setU_0. apply/set0_P => j /Zo_P [jsf [jp jc]]. move: (NS_inc_nat (NS_succ sfN) jsf) => jN. move: (cpred_pr jN (nesym (proj2 jp)))=> [kN kv]. have ksf: inc (cpred j) (source f). apply/(NltP sfN)/(cleSltP kN)/(NleP sfN);ue. exact: (hc _ ksf jc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)