proposition: Lemma Sperner_cf4 f (p := source f): free_rep f -> factorial n = csumb (csucc p) (fun i => cardinal (chain_free_meet_i f i)).
proof: Proof. move => fp. rewrite - csum_pr4_bis; last first. move => i j ip jp; mdi_tac nij => x /Zo_hi iv /Zo_hi jv; case: nij; ue. rewrite - Sperner_14; congr cardinal. set_extens t; last by move =>/setUf_P [y yp] /Zo_S. move => tC; apply/setUf_P. have pN: natp p by case: fp. have zp: inc \0c (csucc p) by apply/(NleP pN); apply: cle0n. case: (Sperner_cf3 fp tC); first by move => h; ex_tac; apply:Zo_i. move => [i [isf pb pc]]. move/(NltP pN): isf => lip; move: (NS_lt_nat lip pN) => iN. have sisip : inc (csucc i) (csucc p) by apply/(NleP pN)/cleSltP. by ex_tac; apply: Zo_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)