proposition: Lemma Exercise5_1 p n q : natp n -> p <=c n -> q <c p -> binom n p = csumb (Nintcc q (n -c p +c q)) (fun k => binom (n-c (csucc k)) (p -c (csucc q)) *c binom k q).
proof: Proof. move => nN lepn ltpq. have pN:= (NS_le_nat lepn nN). have qN:=(NS_lt_nat ltpq pN). set E := (Nint n). set bigset := subsets_with_p_elements p E. have ce: cardinal E = n by exact: (card_Nint nN). pose EV X := select (fun x => cardinal (X \cap (Nint x)) = q) X. have PA:= (card_p_subsets nN pN ce). have PB: forall X, inc X bigset -> exists ! x, inc x X /\ cardinal (X \cap (Nint x)) = q. move => X /Zo_P [] /setP_P XE cx. pose f x := cardinal (X \cap Nint x). have f0: f \0c = \0c by rewrite /f Nint_co00 setI2_0 cardinal_set0. have fn: f n = p by rewrite /f -/E; move /setI2id_Pl: XE => ->. have pa: forall x, natp x -> Nint x +s1 x = Nint (csucc x). move => x xn; exact (proj1 (Nint_pr4 xn)). have pb: forall x, natp x -> X \cap Nint (csucc x) = (X \cap Nint x) \cup (X \cap singleton x). by move => x xb; rewrite - set_IU2r - (pa _ xb). have fnok: forall x, natp x -> ~(inc x X) -> f x = f (csucc x). move => x xB xX; rewrite /f - (pa _ xB); f_equal. set_extens t; move => /setI2_P [sa sb]; apply /setI2_P; split;fprops. by case /setU1_P: sb => // xt; case: xX; rewrite - xt. have fok: forall x, natp x -> (inc x X) -> csucc (f x) = f (csucc x). move => x xB xX; rewrite /f (pb _ xB). have ->: (X \cap singleton x) = singleton x. by apply: set1_pr; fprops => z /setI2_P [_] /set1_P. by rewrite csucc_pr //; move /setI2_P => [_] /(NintP xB) []. have cax: forall x, cardinalp (f x) by rewrite /f; fprops. have fxb x: natp (f x). by apply:NS_le_nat pN; rewrite - cx; apply: sub_smaller;apply: subsetI2l. have fm: forall x y, natp x -> natp y -> f x <=c f (x +c y). move => x y xN yN; move: y yN x xN; apply: Nat_induction. move => x xN; rewrite csum0r; fprops. move => m mN hrec x xb; move: (hrec _ xb) => pc; apply: (cleT pc). rewrite (csum_nS _ mN); case: (inc_or_not (x +c m) X) => h. + rewrite - (fok _ (NS_sum xb mN) h); apply:cleS0; fprops. + rewrite - (fnok _ (NS_sum xb mN) h); fprops. have fm1: forall x y, natp x -> natp y -> x <c y -> inc x X -> f x <c f y. move => x y xN yN /(cleSltP xN) xy xx; move: (fok _ xN xx) => pc. apply /(cleSltP (fxb x)). rewrite - (cdiff_pr xy) pc; apply: fm; fprops. have XN: sub X Nat by move => t tx; exact: (Nint_S1 (XE _ tx)). apply /unique_existence;split; last first. move => x y [xx xv][yx yv] ;move: (XN _ xx) (XN _ yx) => xN yN. case: (cleT_ell (CS_nat xN)(CS_nat yN)) => // ha. by move: (fm1 _ _ xN yN ha xx) => [_]; rewrite /f xv yv. by move: (fm1 _ _ yN xN ha yx) => [_]; rewrite /f xv yv. have lt1: q <c f n by rewrite fn. case: (least_int_prop2 nN lt1 (p := fun k => q <c f k)). by rewrite f0 => /clt0. set x:= cpred _; move =>[xN pe pg]. exists x; case: (inc_or_not x X) => xx; last first. by case: pg; rewrite (fnok _ xN xx). move: pe; rewrite - (fok _ xN xx); move /(cltSleP (fxb x)) => ph. split => //; ex_middle eq1; case: pg; split => //; fprops. have PC: forall X, inc X bigset -> ( cardinal (X \cap (Nint (EV X))) = q /\ inc (EV X) X). move => X xb; move:(PB _ xb) => [z [[za zb] zc]]; apply: select_pr. ex_tac. by move => a b p1 p2 p3 p4; rewrite - (zc _ (conj p1 p2)) (zc _ (conj p3 p4)). have PD: forall X, inc X bigset -> inc (EV X) (Nintcc q (n -c p +c q)). move => X px;move: (PC _ px) => [pc pd]. move: px => /Zo_P [] /setP_P pa pb. have sc: natp ((n -c p) +c q) by fprops. move: (Nint_S1 (pa _ pd)) => xN. set int := (Nint (EV X)). move: (sub_smaller (@subsetI2r X int)); rewrite pc (card_Nint xN) => pe. apply /(Nint_ccP1 qN sc); split => //. have pf: sub (X \cap int) (X \cap E). by move => T /setI2_P [tx ti]; apply /setI2_P;split => //; apply: pa. have pg: cardinal (X \cap E) = p by move /setI2id_Pl: pa => ->. have ph: finite_set (X\cap E) by apply/NatP; rewrite pg. move: (pa _ pd) => /(NintP nN) [ltxn _]. have pf': sub int E by apply:Nint_M1. have ph': finite_set E by apply:finite_Nint. move: (cardinal_setC4 pf' ph'); rewrite (card_Nint nN) (card_Nint xN). move: (cardinal_setC4 pf ph); rewrite pg pc - setIC2 => sa sb. move: (sub_smaller (@subsetI2r X (E -s int))); rewrite sa sb. rewrite (cdiff_pr8 (proj1 ltpq) lepn nN). move => /(cdiff_pr9 (NS_diff q pN) nN xN ltxn); rewrite csumC => ha. have hb:= (cleT (cdiff_ab_le_a q (proj31 lepn)) lepn). by apply/(cdiff_pr9 xN nN (NS_diff q pN) hb). transitivity (csumb (Nintcc q (n -c p +c q)) (fun k => cardinal ( Zo bigset (fun X => EV X = k)))). rewrite - PA; apply:card_partition_induced; apply:PD. apply: csumb_exten => k /Nint_ccP [_ [_ _ lin]]. have ly1: (n -c p +c q) <c n. move: (cdiff_pr lepn); set np := (n -c p) => <-. rewrite csumC; exact: (csum_Mlteq (NS_diff _ nN) ltpq). have ltkn:= cle_ltT lin ly1. have kN:= (NS_lt_nat ltkn nN). have sk:= (NS_succ kN). move / (cleSltP kN): (ltkn) => leskn. move /(cleSltP qN): (ltpq) => lesqp. move: (cdiff_pr lesqp); set q':= (p -c csucc q) => eq1. set I2 := E -s (Nintc k). have i2p:I2 = E -s Nint (csucc k) by rewrite - (Nint_co_cc kN). have ci2: cardinal I2 = (n -c csucc k). have pf': sub (Nint (csucc k)) E by apply: Nint_M1. have ph': finite_set E by apply: finite_Nint. by move: (cardinal_setC4 pf' ph'); rewrite (card_Nint nN) i2p (card_Nint sk). have q'N: natp q' by rewrite /q'; fprops. have nskN: natp (n -c csucc k) by fprops. move: (card_p_subsets kN qN (card_Nint kN)). move: (card_p_subsets nskN q'N ci2). set Y:= subsets_with_p_elements _ _. set Z := subsets_with_p_elements _ _ => <- <-. rewrite cprod2cl cprod2cr cprod2_pr1. symmetry;apply /card_eqP. pose f z := (P z \cup Q z) +s1 k. exists (Lf f (Y \times Z) (Zo bigset (fun X => EV X = k))). have ci2N: natp (cardinal I2) by rewrite ci2; fprops. have la:lf_axiom f (Y \times Z) (Zo bigset (fun X => EV X = k)). move => u /setX_P [pu ] /Zo_P [] /setP_P pa pb /Zo_P [] /setP_P pc pd. have pe: sub ((P u \cup Q u) +s1 k) E. move => t; case /setU1_P. case /setU2_P => ta; first by move /setC_P: (pa _ ta) => []. move: (pc _ ta) => /(NintP kN) tk; apply /(NintP nN). exact:clt_ltT tk ltkn. by move => ->; apply /(NintP nN). have pf: cardinal ((P u \cup Q u) +s1 k) = p. have nku: ~ inc k (P u \cup Q u). move /setU2_P; case => h. move: (pa _ h); rewrite i2p; move=> /setC_P [_]; case. apply/(NintsP kN); fprops. by move: (pc _ h) => /(NintP kN) [_]. rewrite (csucc_pr nku). have di: disjoint (P u) (Q u). apply disjoint_pr => t ta tb. move: (pa _ ta); rewrite i2p; move=> /setC_P [_]; case. by move: (pc _ tb) =>/ (NintP kN) [le1 _]; apply /(NintsP kN). rewrite (csum2_pr5 di) - csum2cr - csum2cl pb pd. rewrite - (csum_nS _ qN) cdiff_rpr //. have pg: inc (f u) bigset by apply /Zo_P; split => //; apply /setP_P. apply /Zo_P; split; first by exact. have ph:inc k (f u) /\ cardinal (f u \cap Nint k) = q. split; first by apply /setU1_P; right. suff: ((P u \cup Q u) +s1 k) \cap Nint k = Q u. by rewrite /f => ->. set_extens t; last by move => ts; apply /setI2_P; split;fprops. move /setI2_P => [sa] /(NintP kN) [tk1 tk2]; case /setU1_P: sa =>//. case /setU2_P => // tp; move: (pa _ tp). by rewrite i2p => /setC_P [te] /(NintsP kN). have pi:inc (EV (f u)) (f u) /\ cardinal (f u \cap Nint (EV (f u))) = q. by move: (PC _ pg)=> [sa sb]. move/unique_existence: (PB _ pg) => [_ h]; exact (h _ _ pi ph). have fi: forall u v, inc u (Y \times Z) -> inc v (Y \times Z) -> f u = f v -> u = v. have aux: forall u, inc u (Y \times Z) -> u = J (f u \cap I2) (f u \cap (Nint k)). move => u /setX_P [pu ] /Zo_P [] /setP_P pa _ /Zo_P [] /setP_P pb _. rewrite - {1} pu /f; congr (J _ _). set_extens t. move => ts; apply /setI2_P; split;fprops. move /setI2_P => [sa]; rewrite i2p => /setC_P [te] /(NintsP kN). move => tk;case /setU1_P: sa. by case /setU2_P => // tq; move /(NintP kN): (pb _ tq) => [tk1 _]. move => tk1; case: tk; rewrite tk1; fprops. set_extens t. move => ts; apply /setI2_P; split;fprops. move /setI2_P => [sa] /(NintP kN) [tk1 tk2]; case /setU1_P: sa =>//. case /setU2_P => // tp; move: (pa _ tp). by rewrite i2p => /setC_P [te] /(NintsP kN). by move => u v pu pv sv; rewrite (aux _ pu) (aux _ pv) sv. saw; apply: lf_bijective => //. move => y /Zo_P [pa pb]. move: (PC _ pa); rewrite pb; move => [pc pd]. set A:=(y \cap Nint k); set B:= (y -s A) -s1 k. have ay: sub A y by apply subsetI2l. have Az: inc A Z by apply /Zo_P;split => //; apply /setP_P; apply: subsetI2r. move: pa => /Zo_P []/setP_P y1 y2. have b2: sub B I2. rewrite i2p;move => t /setC1_P [] /setC_P [ta tb] tc; apply /setC_P. split;fprops; move /(NintsP kN) => tk; case: tb; apply /setI2_P. split => //;by apply /(NintP kN); split. have pa: inc k (y -s A). by apply /setC_P;split => //; move /setI2_P => [_] /(NintP kN) []. move: (cardinal_setC2 ay);rewrite y2 - csum2cl pc - csum2cr. rewrite(csucc_pr2 pa) -/B - eq1. move: (NS_le_nat(sub_smaller b2) ci2N) => cbN. rewrite (csum_nS _ cbN) - (csum_Sn _ qN) => h. move: (csum_eq2l (NS_succ qN) q'N cbN h) => h1. have By: inc B Y by apply /Zo_P;split => //; apply /setP_P. exists (J B A); first by apply:setXp_i. rewrite /f; aw; set_extens t; last first. case /setU1_P; last by move => -> ;apply: pd. by case /setU2_P; [ move => /setC1_P [] /setC_P [] | move /setI2_P=> []]. move => ty; apply /setU1_P;case: (equal_or_not t k) => tk //; first by right. left; apply /setU2_P; case: (inc_or_not t A) => ta; first by right. by left; apply /setC1_P;split => //; apply /setC_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)