proposition: Lemma Exercise5_6 n h (f := fun i => (binom h i) *c (binom (n +c h -c i) h)): natp n -> natp h -> csumb (Nintc_even h) f = \1c +c csumb (Nintc_odd h) f.
proof: Proof. move => nN hN. have izi: inc \0c (Nintc h) by apply/(NintcP hN); apply:(cle0n hN). set A := (Nintc_even h). have za: inc \0c A by apply Zo_i;[ exact:izi | apply: even_zero]. have nzc: ~ inc \0c (A -s1 \0c) by move /setC1_P => []. have fc0: cardinalp (f \0c) by rewrite /f; fprops. have nhN: natp (n +c h) by fprops. rewrite - (setC1_K za) (csumA_setU1 _ nzc) {2} /f (binom0 hN) (cdiff_n0 nhN). set J := (Nint h). pose Ak k := graphs_sum_le J k. pose Bk i := Zo (Ak n) (fun z => Vg z i <> \0c). have cJ: cardinal J = h by rewrite card_Nint. have fsj: finite_set J by apply:finite_Nint. have r1: forall z (k:= cardinal z), sub z J -> nonempty z -> cardinal (intersectionf z Bk) = binom ((n +c h) -c k) h. move => z k zj nez. have ->: (intersectionf z Bk) = Zo (Ak n) (fun f => forall i, inc i z -> Vg f i <> \0c). set_extens v. move /(setIf_P _ nez) => p1. move: (p1 _ (rep_i nez)) => /Zo_P [p2 p3]; apply /Zo_P;split => //. by move => i iz; move: (p1 _ iz) => /Zo_P [_]. move =>/Zo_P [p1 p2]; apply/(setIf_P _ nez) => j jz; apply /Zo_P;fprops. move: (sub_smaller zj); rewrite cJ - /k => kn. move: (NS_le_nat kn hN) => kN. set Z := Zo _ _. pose ga f:= Lg J (fun i => Yo (inc i z) (cpred (Vg f i)) (Vg f i)). pose gb f:= Lg J (fun i => Yo (inc i z) (csucc (Vg f i)) (Vg f i)). have pb : forall f, fgraph f -> allf f cardinalp -> domain f = J -> (forall i, inc i J -> natp (Vg f i)) -> (forall i, inc i z -> Vg f i <> \0c) -> csum (ga f) +c k = csum f. move => g p1 p2 p0 p3 p4. pose f2 := (graph (char_fun z J)). have q2: forall i, inc i J -> Vg (ga g) i +c Vg f2 i = Vg g i. move => i iJ; rewrite /ga /f2 -/(Vf _ i) LgV//; Ytac zi. rewrite (char_fun_V_a zj zi). move: (cpred_pr (p3 _ iJ) (p4 _ zi)) => [h1 h2]. by rewrite -(Nsucc_rw h1) - h2. have aux: inc i (J -s z) by apply /setC_P. by rewrite char_fun_V_b // csum0r //; apply: p2; rewrite p0. set f3 := (Lg J (Vg f2)). have s1: fgraph f3 by rewrite /f3; by fprops. have s2: sub z (domain f3) by rewrite /f3; aw. have s3: forall i, inc i ((domain f3) -s z) -> Vg f3 i = \0c. rewrite /f3/f2; aw => i ij; rewrite LgV//; last by move /setC_P: ij => []. by rewrite -/(Vf _ _) (char_fun_V_b zj ij). move: (csum_zero_unit s2 s3). have ->: csumb z (Vg f3) = csumb z (fun i =>\1c). apply : csumb_exten => i iz; move: (zj _ iz) => iJ; rewrite /f3 LgV//. exact (char_fun_V_a zj iz). rewrite csum_of_ones -/k => s5. move: (sum_of_sums (Vg (ga g)) (Vg f2) J); rewrite /csumb. have r1 : domain (ga g) = J by rewrite /ga; aw. have r3 : fgraph (ga g) by rewrite /ga; fprops. rewrite -{1} r1 (Lg_recovers r3) s5 => ->; f_equal. apply: fgraph_exten; fprops; aw; first by symmetry. move => i ij /=; rewrite LgV//; exact (q2 _ ij). have pa: forall f, inc f Z -> [/\ k <=c n, inc (ga f) (Ak (n -c k)) & gb (ga f) = f]. move => g /Zo_P [p0 p5]. move /(graphs_sum_leP _ nN): (p0) => [p1 p2 p3 p4]. have q1: forall i, inc i J -> natp (Vg g i). rewrite - p1 => i isf. exact: (NS_le_nat (cleT (csum_increasing6 (p4 _ isf) isf) p2) nN). move: (pb _ p3 p4 p1 q1 p5) => q3. have r1 : domain (ga g) = J by rewrite /ga; aw. have q4: k <=c csum g. by rewrite - q3; apply:csum_Mle0; fprops. have q5: k <=c n by apply: (cleT q4 p2). move: (NS_diff k nN) =>q6. have q7: csum (ga g) <=c n -c k. have q4': csum (ga g) <=c csum g. by rewrite - q3; apply:csum_M0le; fprops. move: (NS_le_nat (cleT q4' p2) nN) => h1. move: p2; rewrite -q3 - {1} (cdiff_pr q5) csumC => s1. exact (csum_le2l kN h1 q6 s1). have r3 : fgraph (ga g) by rewrite /ga; fprops. have r4 : allf (ga g) cardinalp. red; rewrite /ga; aw => i ij; rewrite LgV//; move: (q1 _ ij) => ha; Ytac iz; fprops. move: (cpred_pr ha (p5 _ iz)) => [h1 h2]; fprops. have q8: inc (ga g) (Ak (n -c k)). apply (graphs_sum_leP _ q6); split => //; split => //. split => //; rewrite /gb;apply: fgraph_exten; [ fprops | done | by aw | aw]. move => i iJ; rewrite LgV// /ga; Ytac iz; bw => //; Ytac0; last by exact. by rewrite - (proj2 (cpred_pr (q1 _ iJ) (p5 _ iz))). case: (cleT_el (CS_nat kN) (CS_nat nN)) => aux; last first. have ->: Z = emptyset. apply /set0_P => t tz; case: (cltNge aux (proj31 (pa _ tz))). rewrite cardinal_set0 - (cdiff_pr kn); set i := h -c k. move: (NS_diff k hN) => iN. rewrite (csumC k) csumA (cdiff_pr1 (NS_sum nN iN) kN) (csumC i). by rewrite binom_bad //; fprops; apply: csum_Mlteq. have ->: (n +c h) -c k = (n -c k) +c h. rewrite -{1} (cdiff_pr aux) csumC (csumC k) (csumC _ h) csumA cdiff_pr1 //. fprops. move: (proj2 (set_of_functions_sum_pr (NS_diff k nN) hN)). rewrite (binom_symmetric2 (NS_diff k nN) hN) -/(Ak _) => <-. apply /card_eqP; exists (Lf ga Z (Ak (n -c k))); saw. have q6 := (NS_diff k nN). apply: lf_bijective. by move => g fa; move: (pa _ fa)=> [_ ok _]. move => u v uz vz sw; move: (pa _ uz) (pa _ vz) => [_ _ e1][_ _ e2]. by rewrite - e1 -e2 sw. move =>y yf. move /(graphs_sum_leP _ q6): (yf) => [p1 p2 p3 p4]. have q1: forall i, inc i J -> natp (Vg y i). rewrite - p1 => i isf. exact: (NS_le_nat (cleT (csum_increasing6 (p4 _ isf) isf) p2) q6). have q5:forall i, inc i z -> Vg (gb y)i <> \0c. move => i iz; move: (zj _ iz) => iJ;rewrite /gb LgV//; Ytac0. apply: succ_nz. have q4: ga (gb y) = y. move: yf; rewrite /Ak; move /(graphs_sum_leP J q6)=> [s1 s2 s3 s4]. rewrite /ga; apply: fgraph_exten; aww. move => i iJ /=; rewrite LgV// /gb LgV//; Ytac zi; Ytac0; last by exact. by apply: cpred_pr2; apply: q1. have q2: fgraph (gb y) by rewrite /gb; fprops. have dgb: (domain (gb y)) = J by rewrite /gb; aw. have q7: forall i, inc i J -> natp (Vg (gb y) i). move => i ij; move: (q1 _ ij) => ha;rewrite /gb LgV//; Ytac zi; fprops. have q3: (allf (gb y) cardinalp). move => i; rewrite dgb => ij; rewrite /gb LgV//; move: (q1 _ ij) => hw. Ytac zi; fprops. exists (gb y) => //. apply /Zo_P;split => //; apply /(graphs_sum_leP _ nN) => //;split => //. move: (pb _ q2 q3 dgb q7 q5); rewrite q4; move => <-. rewrite - (cdiff_pr aux) csumC; apply: csum_Mlele => //; fprops. set fct0:= cst_graph J \0c. have fct0_ok: inc fct0 (Ak n). apply /graphs_sum_leP => //; rewrite /fct0 Lgd;split => //. by rewrite -/(csumb _ _) csum_of_same cprod0l;apply:cle0n. fprops. hnf; aw; move => t tj; rewrite LgV//; fprops. have ue: (unionf J Bk) = Ak n -s1 fct0. set_extens t. move => /setUf_P [z tz] /Zo_P [ta tb]. apply /setC1_P; split => //; dneg eq2; rewrite eq2 /fct0 LgV//. move => /setC1_P [t1 t2]; apply /setUf_P. move /(graphs_sum_leP _ nN): (t1) => [t4 _ t5 t6]. suff: (exists2 i, inc i J & Vg t i <> \0c). move => [i ij t3]; ex_tac; apply /Zo_P;split => //. ex_middle bad; case: t2; rewrite /fct0. apply: fgraph_exten => //; aww. rewrite t4; move => s st /=; rewrite LgV//; ex_middle ok; case: bad; ex_tac. move: (Exercise5_5_b3 Bk fsj). have cb1: cardinalp (binom (n +c h) h) by apply: CS_nat; apply:NS_binom. move: (csucc_pr2 fct0_ok); rewrite -ue csucc_pr4; last by fprops. rewrite csumC (cprod1l cb1) (binom_symmetric2 nN hN). rewrite (proj2 (set_of_functions_sum_pr nN hN)) => ->. set s1 := csumb _ _;set s2 := csumb _ _. set s3 := csumb _ _; set s4 := csumb _ _. have ->: s2 = s4. have ->: s2 = csumb (odd_card_sub J) (fun z => binom ((n +c h) -c (cardinal z)) h). apply: csumb_exten => t. move => /Zo_P [] /setP_P ta tb; apply: r1 => //. by apply: odd_nonempty. set X := (odd_card_sub J); set F := Nintc_odd h. have pa: (forall x, inc x X -> inc (cardinal x) F). move => x /Zo_P [] /setP_P pa pb; apply /Zo_P;split => //. apply /(NintcP hN); rewrite - cJ; apply:(sub_smaller pa). rewrite (card_partition_induced1 _ pa). apply: csumb_exten => i iF. set Y:= Zo _ _. transitivity (csumb Y (fun _ => (binom ((n +c h) -c i) h))). by apply: csumb_exten => j jY /=; move /Zo_P: jY => [_ ->]. rewrite csum_of_same cprodC - cprod2cl. move /Zo_P: iF => [i1 i2]; move: (Nint_S i1) => i3. have ->: Y = subsets_with_p_elements i J. set_extens t. move => /Zo_P [] /Zo_P [t1 t2] t3; apply /Zo_P;split => //. move => /Zo_P [t1 t2]; apply/Zo_P;split => //. by apply /Zo_P;split => //; rewrite t2. by rewrite (card_p_subsets hN i3 cJ). have ->: s1 = s3. have ->: s1 = csumb (even_card0_sub J) (fun z => binom ((n +c h) -c (cardinal z)) h). apply:csumb_exten => t. by move => /setC1_P [/Zo_P[/setP_P ta tb]] /nonemptyP tne; apply: r1. set X := (even_card0_sub J); set F := (A -s1 \0c). have pa: (forall x, inc x X -> inc (cardinal x) F). move => x /setC1_P [/Zo_P[/setP_P wJ pa]] pb; apply /Zo_P; split. apply /Zo_P;split => //;apply /(NintcP hN). rewrite - cJ; apply:(sub_smaller wJ). by move /set1_P=> /card_nonempty. rewrite (card_partition_induced1 _ pa). apply: csumb_exten => i iF. set Y:= Zo _ _. transitivity (csumb Y (fun _ => (binom ((n +c h) -c i) h))). by apply: csumb_exten => j jY /=; move /Zo_P: jY => [_ ->]. rewrite csum_of_same cprodC - cprod2cl. move /Zo_P: iF => [] /Zo_P [i1 i2] /set1_P i3; move: (Nint_S i1) => i4. have ->: Y = subsets_with_p_elements i J. set_extens t. by move => /Zo_P [] /Zo_P [] /Zo_P [t1 t2] t3 t4; apply /Zo_P. move => /Zo_P [t1 t2]; apply/Zo_P;split => //; apply /Zo_P;split => //. by apply /Zo_P;split => //; rewrite t2. by move => /set1_P => te; case: i3; rewrite - t2 te cardinal_set0. by rewrite (card_p_subsets hN i4 cJ). by rewrite (csumC s3) - csumA => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)