proposition: Lemma sum_of_binomial2 a b n: natp n -> csumb (csucc n) (fun p => (binom n p) *c (a ^c p) *c (b ^c (n -c p))) = (a +c b) ^c n.
proof: Proof. move: n; apply: Nat_induction. rewrite succ_zero csumb1 binom00 cdiff_nn ! cpowx0. by rewrite !(cprod1r CS1) (card_card CS1). move=> n nN. have snN:= (NS_succ nN). rewrite {1} /csumb; set fn := Lg _ _ => hrec. set X:=((a +c b) ^c n). pose I := csucc n. have IN:sub I Nat by apply: NS_inc_nat. pose q0 i := (a ^c i) *c (b ^c (n -c i)). pose q1 i := (a ^c (csucc i)) *c (b ^c ((csucc n) -c (csucc i))). pose f1 i := (binom n (csucc i)) *c (q1 i). pose f2 i := (binom n i) *c (q1 i). pose g1 i := (binom n i) *c (a ^c i) *c (b ^c ((csucc n) -c i)). have P1: csumb I f2 = a *c X. pose g i:= a *c (binom n i) *c (q0 i); rewrite /csumb. have ->: Lg I f2 = Lg I g. apply: Lg_exten. move=> x xi; rewrite /f2 /g (cprodC a _) - cprodA. congr (_ *c _); rewrite cprodC /q1 /q0 (cdiff_pr6 nN (IN _ xi)). by rewrite (cpow_succ _ (IN _ xi))- !cprodA (cprodC a). rewrite /X -hrec /fn cprod2Dn; apply: csumb_exten. move=> x xI /=; aw; rewrite cprodA cprodA - cprodA //. have P2: csum (Lg I g1) = b *c X. set (g:= fun i=> b *c ((binom n i) *c (q0 i))). have ->: Lg I g1 = Lg I g. apply: Lg_exten. move=> x /(NleP nN) xi; rewrite /g1/g (cprodC b _). rewrite - cprodA - cprodA - cprodA. by rewrite (cdiffSn nN xi) (cpow_succ _ (NS_diff x nN)). rewrite /X -hrec /fn cprod2Dn;apply: csumb_exten. by move=> x xI /=; aw; rewrite - (cprodA (binom n x)). rewrite (fct_sum_rec1 _ snN). have a1: cardinalp (b ^c (csucc n)) by fprops. rewrite (binomSn0 nN) cpowx0 (cdiff_n0 snN) (cprod1l CS1) (cprod1l a1). set ffn:= fun i => _. have <-: (g1 \0c) = (b ^c (csucc n)). rewrite /g1 cpowx0 (cdiff_n0 snN) (binom0 nN). by rewrite (cprod1l CS1)(cprod1l (CS_pow b (csucc n))). have <-:csumb I (fun i => (f1 i) +c (f2 i)) = (csumb I ffn). apply: csumb_exten => i iI. by rewrite /ffn -/(q1 i) /f1 /f2 (binomSnSm nN (IN _ iI)) - cprodA cprodDl. rewrite -/(csumb _ _) -(sum_of_sums f1 f2 I) P1 (csumC _ (a *c X)) - csumA. have <-: csumb (csucc n) (fun i=> g1 (csucc i)) = (csumb I f1). apply: csumb_exten=> u uI; rewrite /f1 /g1 - cprodA //. rewrite -(fct_sum_rec1 g1 snN). have ->: csumb (csucc (csucc n)) g1 = b *c X. have aux:= (cltS nN). rewrite (csum_fs _ snN) {2}/g1 (binom_bad nN snN aux). rewrite 2! cprod0l csum0r //; apply: CS_csum. rewrite - cprodDl cprodC (Nsucc_rw nN) cpow_sum2 cpowx1; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)