proposition: Lemma F27_b n: (\sum_(i < n.+1) i* 'C(n, i) = n * 2 ^ (n.-1) ) %N.
proof: Proof. apply: intmul_inj. move: (refl_equal((deriv (('X + 1%:P) ^+ n):{poly int}).[1%Z])). rewrite {1} addrC exprDn_comm; last by apply: commr_polyX. rewrite deriv_exp derivD derivX derivC addr0 mul1r hornerMn horner_exp. rewrite! hornerE - mulr2n - natrX - mulrnA mulnC pmulrn /=. rewrite raddf_sum /= horner_sum sumMz; move => <-; apply: eq_bigr => i _. by rewrite expr1n mul1r !derivE !hornerMn hornerXn expr1n - mulrnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)