proposition: Lemma Sperner_cf5 f (p := source f) (m := fun i => cardinal (chain_free_meet_i f i)): free_rep f -> cn *c factorial n = cn *c (m \0c) +c csumb p (fun i => cn *c (m (csucc i))).
proof: Proof. move => h; rewrite(f_equal (cprod2 cn) (Sperner_cf4 h)). have pN: natp p by case: h. have zi: inc \0c (csucc p) by apply/(NleP pN); apply: cle0n. rewrite cprod2Dn (fct_sum_rec1 _ pN); aw; rewrite csumC. by apply: f_equal; apply: csumb_exten => i isf; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)