proposition: Lemma sum_of_gen_binom E F n: natp n -> cardinal E = n -> csumb (graphs_sum_eq F n) (fun p => cardinal (partitions_pi p E)) = (cardinal F) ^c n.
proof: Proof. move=> cE cEn. rewrite - {2}cEn cpowcr cpowcl. pose g f i:= (Vfi1 f i). pose f1 f := (Lg F (fun i=> cardinal (g f i))). pose f2 f := Lg F (g f). have p1: forall f, inc f (functions E F) -> (inc (f1 f) (graphs_sum_eq F n) /\ inc (f2 f) (partitions_pi (f1 f) E)). move=> f /functionsP [ff sf tf]. have sfa: (source f = unionb (Lg (target f) (g f))). set_extens t. move => tsf; apply /setUb_P; aw. have Wt := (Vf_target ff tsf). ex_tac; rewrite LgV//; apply /iim_fun_set1_i => //. move => /setUb_P; aw; move => [y ytg]; rewrite LgV// => h. by case /(iim_fun_set1_P _ ff): h. have md: mutually_disjoint (Lg (target f) (g f)). apply: mutually_disjoint_prop2 => i j y itf jtf pa pb. by rewrite (iim_fun_set1_hi ff pa) (iim_fun_set1_hi ff pb). split; last first. rewrite /f1 /f2;apply /partitions_piP; hnf; saw. move => i iF; rewrite !LgV//. hnf; rewrite -tf;split;fprops; ue. rewrite /f1; apply /(graphs_sum_eqP _ cE);aw; rewrite /cardinal_fam /allf. split; [exact | rewrite - cEn - sf sfa | fprops |]. apply: Eqc_disjointU => //. rewrite /disjointU_fam; hnf;aw; split;fprops. move=> i itf; rewrite !LgV//; aw; trivial;ue. apply: mutually_disjoint_prop2; aw => i j y pa pb; aw. rewrite !LgV //. by move /indexed_P => [_ _ <-] /indexed_P [_ _ <-]. aw => i iF; rewrite LgV//; fprops. set G:= Lg (graphs_sum_eq F n) (fun p => (Zo (functions E F) (fun f=> f1 f = p))). have g1: unionb G = (functions E F). rewrite /G; set_extens f. by move /setUb_P ;aw; move => [y ys]; rewrite LgV//; move /Zo_P => []. move => fsf ;move: (p1 _ fsf) => [fa fb]; apply /setUb_P; aw. by ex_tac;rewrite LgV//; apply: Zo_i. have g2: mutually_disjoint G. by apply: mutually_disjoint_prop2 => i j y ip jp /Zo_hi <- /Zo_hi <-. symmetry; rewrite /cpow -g1. apply: Eqc_disjointU; fprops; rewrite /G/disjointU_fam; saw. move=> p pd; rewrite !LgV//; aw. apply/card_eqP. set X:= Zo _ _. exists (Lf f2 X (partitions_pi p E)); saw. apply: lf_bijective. by move=> t /Zo_P [ts <-]; move: (p1 _ ts) => []. move=> u v /Zo_P [] /functionsP [fu su tu] f1u /Zo_P [] /functionsP [fv sv tv] f1v Weq. apply: function_exten =>//; try ue. move=> x xsu /=. have WF: inc (Vf u x) F by Wtac. move: (f_equal (Vg ^~(Vf u x)) Weq); rewrite /f2 /g !LgV// => ieq. have : (inc x (Vfi1 u (Vf u x))). by apply: iim_fun_set1_i. by rewrite ieq; move /(iim_fun_set1_hi fv). move=> y /partitions_piP ys. have pip0 := (pip_prop0 ys). have [df cVg [fgf duj ue]] := ys. have doi: domain p = F by move /(graphs_sum_eqP _ cE): pd => []. rewrite doi in cVg. pose xf x := select (fun j => inc x (Vg y j)) F. have xfp: forall x, inc x E -> inc x (Vg y (xf x)) /\ (inc (xf x) F). move => x xE;apply: select_pr. by move: xE;rewrite -ue => /setUb_P; rewrite df doi. rewrite - doi - df. move => a b /= aF va bF vb; case:(duj a b aF bF) => //. move => di;empty_tac1 x. have ta: lf_axiom xf E F by move=> t tE; case:(xfp _ tE). set x:= Lf xf E F. have fx: function x by apply: lf_function. have xsf: inc x (functions E F) by apply /functionsP; rewrite /x;hnf;aw. have xp1: forall t, inc t F -> g x t = Vg y t. move=> t tF; set_extens u. move /(iim_fun_set1_P _ fx) => []; rewrite lf_source => uE. rewrite /x LfV // => -> ; apply : (proj1 (xfp _ uE)). move=> uW. have usx: inc u (source x). by rewrite -doi - df in tF; rewrite /x; aw; apply: (pip0 _ tF). apply:(iim_fun_set1_i fx usx). move: usx; rewrite /x lf_source => uE; rewrite LfV//. have [tv vF]:= (xfp _ uE). move: duj; rewrite /mutually_disjoint;aw; rewrite df doi. move=> aux; case: (aux _ _ tF vF) => // d. empty_tac1 u. have xp2: Lg F (g x) = y. symmetry; apply: fgraph_exten =>//; aww; rewrite df //. by rewrite doi; move => u uF /=; rewrite LgV////; rewrite - xp1 //. exists x=>//; apply: Zo_i =>//. move: pd => /(graphs_sum_eqP _ cE) [ pa pb pc pd]. apply: fgraph_exten; rewrite /f1; aww. move => a aF /=; rewrite !LgV//. rewrite xp1 // cVg //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)