proposition: Lemma nderiv_taylor p x h : GRing.comm x h -> p.[x + h] = \sum_(i < size p) p^`N(i).[x] * h ^+ i.
proof: Proof. move/commrX=> cxh; elim/poly_ind: p => [|p c IHp]. by rewrite size_poly0 big_ord0 horner0. rewrite hornerMXaddC size_MXaddC. have [-> | nz_p] := eqVneq p 0. rewrite horner0 !simp; have [-> | _] := c =P 0; first by rewrite big_ord0. by rewrite size_poly0 big_ord_recl big_ord0 nderivn0 hornerC !simp. rewrite big_ord_recl nderivn0 !simp hornerMXaddC addrAC; congr (_ + _). rewrite mulrDr {}IHp !big_distrl polySpred //= big_ord_recl /= mulr1 -addrA. rewrite nderivn0 /bump /(addn 1) /=; congr (_ + _). rewrite !big_ord_recr /= nderivnMXaddC -mulrA -exprSr -polySpred // !addrA. congr (_ + _); last by rewrite (nderivn_poly0 (leqnn _)) !simp. rewrite addrC -big_split /=; apply: eq_bigr => i _. by rewrite nderivnMXaddC !hornerE_comm /= mulrDl -!mulrA -exprSr cxh. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)