proposition: Lemma F28 n: \sum_(i < n.+1) with_sign i (i* 'C(n, i)) = if n is 1 then -1%:Z else 0.
proof: Proof. case:n; first by rewrite big_ord_recl big_ord0 //. case; first by rewrite 2!big_ord_recl big_ord0 //. move => n;move: (refl_equal((deriv (('X + 1%:P) ^+ n.+2):{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_comm addNr /= exprS mul0r mul0rn raddf_sum /= horner_sum. rewrite -{4}(oppr0) ; set g := \sum_(i<_) _; set f := \sum_(i<_) _. move => <- /=; rewrite - sumrN; apply eq_bigr => i _. rewrite expr1n mul1r !derivE !hornerMn hornerXn - 2!mulNrn - mulrnA. case:i =>i _ /=; case: i => // i /=; rewrite exprS mulN1r //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)