proposition: Lemma Sperner_cf7 f i (a := cardinal (Vf f i)) (m := cardinal (chain_free_meet_i f (csucc i))): free_rep f -> inc i (source f) -> natp m /\ m = factorial a *c factorial (n -c a).
proof: Proof. move => fp isf; move: (Sperner_cf0 fp isf) =>[sE _ aN]. rewrite /m (Sperner_cf6 fp isf) (Sperner_19 sE); split => //. apply: NS_prod; apply:NS_factorial => //; apply: (NS_diff _ Sperner_p0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)