proposition: Lemma F27_a n: \sum_(i < n.+1) i* 'C(n, i) = n * 2 ^ (n.-1) .
proof: Proof. elim:n; first by rewrite big_ord_recr big_ord0 mul0n //. move => n Hrec; rewrite big_ord_recl mul0n add0n /= big_split /=. have ->: \sum_(i < n.+1) 'C(n.+1, bump 0 i) = \sum_(i < n.+1) 'C(n, bump 0 i) + \sum_(i < n.+1) 'C(n,i). rewrite - big_split /=; apply: eq_bigr; move => [i lin] _ //=. rewrite addnAC pascal11 mulSnr; congr (_ + _). have ->: n * 2 ^ n = n * 2 ^ n.-1 + n * 2 ^ n.-1. by case n => // m /=; rewrite addnn - muln2 expnSr mulnA. rewrite [X in _ + X] (_ :_ = \sum_(i < n.+1) i*'C(n, bump 0 i) + n * 2 ^ n.-1). rewrite addnA - {2} Hrec; congr (_ + _);rewrite - big_split /=. rewrite [X in _ = X] big_ord_recl big_ord_recr bin_small //=. rewrite mul0n muln0 !addn0 add0n; apply: eq_bigr => i _ /=; rewrite -mulSn //. by rewrite - Hrec - big_split /=; apply: eq_bigr => i _; rewrite - mulnDr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)