proposition: Lemma Exercise5_3b n p: natp n -> natp p -> csumb (Nintc p) (Exercise5_3V n p) = \2c ^c p *c binom n p.
proof: Proof. move => nN pN. set E := Nint n. set F :=subsets_with_p_elements p E. have ce: cardinal E = n by apply:(card_Nint nN). set rhs := \2c ^c p *c binom n p. set EE := (\Po E \times \Po E). set G1 := Zo EE (fun z => inc (P z) F /\ sub (Q z) (P z)). have res1: cardinal G1 = rhs. pose phi := Lf P G1 F. have sp: G1 = source phi by rewrite /phi; aw. have tp: F = target phi by rewrite /phi; aw. rewrite /rhs -(card_p_subsets nN pN ce) -/F tp sp cprodC. have lfa: lf_axiom P G1 F by move => t /Zo_P [_ []]. have fphi: function phi by apply: lf_function. apply:(shepherd_principle fphi). move => x; rewrite - tp => xf. set K := Vfi1 _ _. pose f := Lf (fun z => J x z) (\Po x) K. move /Zo_P: (xf) => [] /setP_P xE cx. suff bf: bijection f. by move: (card_bijection bf); rewrite - cx cpowcr - card_setP /f; aw. apply lf_bijective. - move => y /setP_P yx. have aux: inc (J x y) G1. apply /Zo_P; saw => //; apply: setXp_i; apply /setP_P => //. apply: (sub_trans yx xE). apply :(iim_fun_set1_i fphi); rewrite /phi? LfV//; aw; trivial. - move => u v _ _ h; exact (pr2_def h). - move => y /(iim_fun_set1_P _ fphi) []; rewrite - sp => yG. move /Zo_P: (yG) => [pa [pb pc]]; rewrite /phi LfV// => ->; exists (Q y). by apply /setP_P. by rewrite (setX_pair pa). set G2 := Zo EE (fun z => [/\ cardinal (P z) <=c p, cardinal (Q z) = p -c cardinal (P z) & sub (Q z) (E -s (P z))]). have fse: finite_set E by apply: finite_Nint. have res2: cardinal G2 = rhs. rewrite - res1; symmetry; apply /card_eqP. exists (Lf (fun z => J (Q z) ((P z) -s (Q z))) G1 G2);saw. apply: lf_bijective. - move => z /Zo_P [] /setX_P [pz Pz Qz] [/Zo_P [_ pc] pb]; apply /Zo_P; aw. move /setP_P:Pz => pze; move: (sub_finite_set pze fse) => fsp. split; last split. + by apply: setXp_i => //; apply /setP_P => t /setC_P [pa _]; apply: pze. + by move: (sub_smaller pb); rewrite pc. + by rewrite (cardinal_setC4 pb fsp) pc. + by move /setP_P:Qz => qze t /setC_P [ta tb]; apply /setC_P;split;fprops. - move => u v /Zo_P [pa [_ pb]] /Zo_P [pc [_ pd]] eq1. rewrite - (setX_pair pa) - (setX_pair pc) - (setU2_Cr pb) - (setU2_Cr pd). by rewrite (pr2_def eq1) (pr1_def eq1). - move => y /Zo_P [] /setX_P [pa Py /setP_P Qy] [pb pc pd]. have a0 : ((P y \cup Q y) -s P y) = Q y. set_extens t; first by move => /setC_P [] /setU2_P; case. move => tq; apply /setC_P; split;fprops => py. by case/setC_P: (pd _ tq). have aux: J (P y) ((P y \cup Q y) -s P y) = y by rewrite - [RHS] pa a0. have a2:= @subsetU2l (P y) (Q y). move: (Py) => /setP_P Py'. have a3:inc (P y \cup Q y) (\Po E) by apply /setP_P/setU2_12S. have a4:inc (P y \cup Q y) F. apply :Zo_i => //; rewrite (cardinal_setC2 a2) a0 - csum2cr - csum2cl. by rewrite pc; apply: cdiff_pr. exists (J (P y \cup Q y) (P y)); aw; last by rewrite a0 pa. by apply /Zo_P; aw;split; [ apply: setXp_i | ]. pose Xk k := Zo EE (fun z => [/\ cardinal (P z) = k, cardinal (Q z) = p -c cardinal (P z) & sub (Q z) (E -s P z)]). set X := Lg (Nintc p) Xk. have X1: fgraph X by rewrite /X; fprops. have X2: mutually_disjoint X. red;rewrite /X; aw => i j ip jp; rewrite !LgV//;mdi_tac nij => u ua ub; case: nij. by move: ua ub => /Zo_hi [<- _ _] /Zo_hi [<- _ _]. have X3: (unionb X) = G2. rewrite /X;set_extens t. move /setUb_P; aw; move => [y yp]; rewrite LgV//; move /Zo_P => [p1 [p2 p3 p4]]. by apply /Zo_i => //; rewrite p3 p2; split => //;apply /(NintcP pN). move /Zo_P=> [p1 [p2 p3 p4]]; apply /setUb_P;aw. by move /(NintcP pN): p2 => h; ex_tac; rewrite LgV//; apply /Zo_P. move: (csum_pr4 X2); rewrite X3 res2 => ->. rewrite /X; aw; symmetry;apply:csumb_exten. move => k kp; move: (kp) => /(NintcP pN) kp1; rewrite LgV// ;exact:Exercise5_3a. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)