proposition: Lemma Lubell_Yamamoto_Meshalkin A (b := fun k => cardinal (Zo A (fun z => cardinal z = k))): (inc A (free_subsets r)) -> csumb (csucc n) (fun k => (b k) *c ((factorial k) *c (factorial (n-c k)))) <=c factorial n.
proof: Proof. move/free_rep_prop1 => [f frp tf]. pose c k:= (factorial k) *c (factorial (n-c k)). pose a i := cardinal (Vf f i). pose m i := cardinal (chain_free_meet_i f (csucc i)). move: (frp) => [bf pN /free_subsetsP/proj1 sts]. move: (Sperner_cf4 frp); rewrite (fct_sum_rec1 _ pN). set s1 := csumb _ _; set s2 := cardinal _; move => eq1. have cs1: cardinalp s1 by apply: CS_cardinal. set s3 := csumb _ _. move: (@csum_M0le s1 s2 cs1); rewrite - eq1; clear s2 eq1 cs1. suff: s1 = s3 by move ->. transitivity ( csumb (source f) (fun i => c (a i))). apply: csumb_exten => i iip. by rewrite (proj2 (Sperner_cf7 frp iip)). have cb t: inc t A -> inc (cardinal t) (csucc n). rewrite -tf; move => /sts tA; apply/(NleP (Sperner_p0)). by move:tA; rewrite (proj2 (subp_osr E)) => /setP_P /sub_smaller. move: (proj1(proj1 bf)) => ff. pose X := Lg A (fun i => c (cardinal i)). have ha: target f = domain X by rewrite /X; aw. transitivity (csum (X \cf graph f)). rewrite /composef (domain_fg ff); apply: csumb_exten. move => i isf; rewrite /X -/(Vf f i) LgV//; Wtac. pose g k := Zo A (fun z => cardinal z = k). have pfg: partition_w_fam (Lg (csucc n) g) (domain X). rewrite - ha tf; split. - fprops. - hnf; aw;move => u v isn vsn; rewrite !LgV//; mdi_tac ww. by move => t /Zo_P [_ ct] /Zo_P [_ ct']; case:ww; rewrite - ct ct'. - set_extens t. by move => /setUb_P; aw; move => [y ysb]; rewrite !LgV//; move/Zo_S. move => tA; move: (cb t tA) => cc;apply/setUb_P; aw; ex_tac; rewrite LgV//. by apply:Zo_i. rewrite - (csum_Cn ha bf) (csum_An pfg); aw; apply: csumb_exten=> i lin /=. rewrite LgV// cprodC cprod2cr -/(g i) - csum_of_same; apply: csumb_exten. move => k /Zo_P [kA <-]; rewrite /X LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)