proposition: Lemma Exercise5_2_alt n: natp n -> n <> \0c -> csumb (Nintc_even n) (binom n) = csumb (Nintc_odd n) (binom n).
proof: Proof. move => nN nz. set E := Nint n. have fsE: finite_set E by apply:finite_Nint. have nE: nonempty E. by exists \0c; apply/NintP; fprops; apply:card_ne0_pos; fprops. move: (Exercise5_2 fsE nE) => /card_eqP. move => h. have cE: cardinal E = n by apply: card_Nint. have En: E = n by apply: NintE. set fe := Lg (Nintc_even n) (fun p => (subsets_with_p_elements p n)). have ha: forall i, inc i (Nintc_even n) -> cardinal (Vg fe i) = binom n i. rewrite /fe => i id; rewrite LgV//. move/Zo_S:id => /(NintcP nN) lin; move:(NS_le_nat lin nN) => iN. by rewrite - (card_p_subsets nN iN cE) En. have hb: (even_card_sub E) = unionb fe. rewrite /fe En;set_extens t. move /Zo_P => [/setP_P te ce]; apply/setUb_P. have ww: inc (cardinal t) (Nintc_even n). apply /Zo_P; split => //. apply/(NintcP nN); rewrite - cE; apply:sub_smaller; ue. by aw; ex_tac; rewrite LgV//; apply/Zo_P;split => //; apply/setP_P. move => /setUb_P; aw; move => [y yi]; rewrite LgV// => /Zo_P [ta tb]. by apply/Zo_P; split => //; rewrite tb;move: (Zo_hi yi). have hc:(mutually_disjoint fe). apply: mutually_disjoint_prop; rewrite /fe; aw => i j y iA jA; rewrite !LgV//. by move=> /Zo_hi <- /Zo_hi <-. set fo := Lg (Nintc_odd n) (fun p => (subsets_with_p_elements p n)). have ha': forall i, inc i (Nintc_odd n) -> cardinal (Vg fo i) = binom n i. rewrite /fo; aw;move => i id; rewrite LgV//. move/Zo_S:id => /(NintcP nN) lin; move:(NS_le_nat lin nN) => iN. by rewrite - (card_p_subsets nN iN cE) En. have hb': (odd_card_sub E) = unionb fo. rewrite /fo En;set_extens t. move /Zo_P => [/setP_P te ce]; apply/setUb_P. have ww: inc (cardinal t) (Nintc_odd n). apply /Zo_P; split => //. apply/(NintcP nN); rewrite - cE; apply:sub_smaller; ue. by aw; ex_tac; rewrite LgV// ; apply/Zo_P;split => //; apply/setP_P. move => /setUb_P; aw; move => [y yi]; rewrite LgV// => /Zo_P [ta tb]. by apply/Zo_P; split => //; rewrite tb;move: (Zo_hi yi). have hc':(mutually_disjoint fo). apply: mutually_disjoint_prop; rewrite /fo; aw => i j y iA jA; rewrite !LgV//. by move=> /Zo_hi <- /Zo_hi <-. transitivity (cardinal (even_card_sub E)). move: (csum_pr4 hc); rewrite - hb {1}/fe => ->. by aw; apply:csumb_exten => t ti; symmetry; apply:ha. move: (csum_pr4 hc'); rewrite h - hb' {1}/fo => ->. by aw; apply:csumb_exten => t ti; apply:ha'. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)