proposition: Lemma nderiv_taylor_wide n p x h : GRing.comm x h -> size p <= n -> p.[x + h] = \sum_(i < n) p^`N(i).[x] * h ^+ i.
proof: Proof. move/nderiv_taylor=> -> le_p_n. rewrite (big_ord_widen n (fun i => p^`N(i).[x] * h ^+ i)) // big_mkcond. apply: eq_bigr => i _; case: leqP => // /nderivn_poly0->. by rewrite horner0 simp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)