proposition: Lemma Sperner_cf8 f (p := source f) (m := fun i => cardinal (chain_free_meet_i f i)) (s := csumb p (fun i => cn *c (m (csucc i)))): free_rep f -> [/\ natp s, p *c factorial n <=c s & (p *c factorial n = s -> forall i, inc i p -> cn *c m (csucc i) = factorial n)].
proof: Proof. move => fp. have nN := Sperner_p0. pose a i := cn *c m (csucc i); pose b i := a i -c factorial n. have ncN: natp cn by apply: (NS_binom nN (NS_half _)). have bN i: inc i p -> natp (b i). by move/(Sperner_cf7 fp) => /proj1 h; apply: NS_diff; apply: NS_prod. have aux i: inc i p -> factorial n +c b i = a i. move => ip; apply: cdiff_pr. rewrite /a /m(proj2 (Sperner_cf7 fp ip)); apply:(Sperner_b1 nN). move:fp =>[/proj1/proj1 ff _ /Sperner_p4/proj1 h ]. by move:(h _ (Vf_target ff ip)) => /setP_P/sub_smaller. have eq1: s = p *c factorial n +c csumb p b. rewrite cprodC - csum_of_same (sum_of_sums _ b p). by apply: csumb_exten => i lip; rewrite (aux _ lip). have pN:= (proj32 fp). have fN := (NS_factorial nN). have p1N: natp (p *c factorial n). apply: (NS_prod pN fN). have p2N: natp (csumb p b). have fsp := (finite_set_nat pN). apply:finite_sum_finite; split; rewrite /allf;aw; trivial. move => i ip; rewrite LgV//; exact: (bN _ ip). have sN: natp s by rewrite eq1; apply: (NS_sum). move: (csum2_compare_spec p1N p2N eq1) =>[ea eb]; split => // ec i ip. move /csum_zero_unit_bis : (eb ec) => h; move: (h i); aw; rewrite LgV// => h1. by move: (aux _ ip); rewrite -/(b i) (h1 ip) (csum0r (CS_nat fN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)