proposition: Lemma Sperner_cf1 f C i: free_rep f -> inc C Sperner_mx_chain -> inc i (source f) -> inc (Vf f i) C -> chain_free_meet f C = csucc i.
proof: Proof. move => [[[ff fi] _] sfN rrf] Cp lin h. rewrite /chain_free_meet; set T := Zo _ _. suff: T = singleton (csucc i) by move ->; rewrite setU_1. move: (Vf_target ff lin) => pa. move: (NS_inc_nat sfN lin) => iN. apply: set1_pr. apply: (Zo_i); first by apply/(NleP sfN)/(cleSltP iN) /(NltP sfN). rewrite (cpred_pr2 iN); split => //; apply: succ_positive. move => j /Zo_P [jsf [jn0 jp]]. move: (NS_inc_nat (NS_succ sfN) jsf) => jN. move: (cpred_pr jN (nesym (proj2 jn0)))=> [kN kv]. have ksf: inc (cpred j) (source f). apply/(NltP sfN)/(cleSltP kN)/(NleP sfN);ue. have vtt: inc (Vf f (cpred j)) (target f) by Wtac. rewrite kv; apply: f_equal. move/Zo_P: Cp => [/total_subordersP [C1 [_ C3]] _]. move: (subp_osr E) => [or sr]. move: (C3 (Vf f i) (Vf f (cpred j))); rewrite iorder_sr // => h1. move/Zo_P: rrf => [ _ h2]. case: (h1 h jp) => /iorder_gle1 cp. by move: (fi _ _ lin ksf (h2 _ _ pa vtt cp)). by move: (fi _ _ ksf lin (h2 _ _ vtt pa cp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)