proposition: Lemma nder_sum n: \sum_(i< n.+1) 'C(n,i) * nder i = n `!.
proof: Proof. elim:n; first by rewrite big_ord_recl big_ord0 //. move => n Hr. have np: 0< n.+1 by []. rewrite big_ord_recl /= bin0 nder0 mul1n (bigID (fun i : 'I_n.+1 => odd i)) /=. have ->: \sum_(i < n.+1 | odd i) 'C(n.+1, bump 0 i) * nder (bump 0 i) = \sum_(i < n.+1 | odd i) 'C(n.+1,i.+1) + \sum_(i < n.+1 | odd i) 'C(n.+1,i.+1) * ((i.+1) *(nder i)). rewrite addnC -big_split /=. by apply:eq_big=> //[[i lin]] /= oi; rewrite nderS' oi /bump add1n addnC mulnS. rewrite 2! addnA. have <-: 2^n = 1 + \sum_(i < n.+1 | odd i) 'C(n.+1, i.+1). rewrite - (F25 np) big_mkcond big_ord_recl /= bin0 // -big_mkcond; congr addn. by apply:eq_big=> // i /=; case: odd. have ->:2 ^ n = \sum_(i < n.+1 | ~~ odd i) 'C(n.+1, i.+1). rewrite - (F24 np) big_mkcond big_ord_recl /= add0n -big_mkcond //. rewrite addnAC -big_split /=. have ->: \sum_(i < n.+1 | ~~ odd i) ('C(n.+1, i.+1) + 'C(n.+1, bump 0 i) * nder (bump 0 i)) = \sum_(i < n.+1 | ~~odd i) 'C(n.+1, i.+1) * (i.+1 * nder i). apply: eq_big => // [[i lin]] /= oi; rewrite nderS' (negbTE oi). by rewrite - mulnS prednK // muln_gt0 /= nbder_even_gt0. rewrite addnC - (bigID (fun i : 'I_n.+1 => odd i) predT) /=. transitivity ( \sum_(i < n.+1) (n.+1) * ('C(n, i) *nder i)). by apply:eq_big => // [[i lin]] /= _; rewrite !mulnA mul_bin_diag (mulnC i.+1). by rewrite - big_distrr /= Hr factS. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)