proposition: Lemma Sperner_cf6 f i: free_rep f -> inc i (source f) -> chain_free_meet_i f (csucc i) = (Zo Sperner_mx_chain (inc (Vf f i))).
proof: Proof. move => fp mip. have aux k: inc k (source f) -> cardinalp k. move => ik; exact (CS_nat (NS_inc_nat (proj32 fp) ik)). set_extens t => /Zo_P [qa qb]; apply/Zo_P; split => //. case:(Sperner_cf3 fp qa); rewrite qb; first by move => qd;case:(@succ_nz i). by move =>[j [/aux jsf fj]] /(csucc_inj (aux _ mip) jsf) => ->. by move: (Sperner_cf1 fp qa mip qb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)