proposition: Lemma Derivation_horner p x : p \is a polyOver E -> x \in E -> D p.[x] = (map_poly D p).[x] + p^`().[x] * D x.
proof: Proof. move=> Ep Ex; elim/poly_ind: p Ep => [|p c IHp] /polyOverP EpXc. by rewrite !(raddf0, horner0) mul0r add0r. have Ep: p \is a polyOver E. by apply/polyOverP=> i; have:= EpXc i.+1; rewrite coefD coefMX coefC addr0. have->: map_poly D (p * 'X + c%:P) = map_poly D p * 'X + (D c)%:P. apply/polyP=> i; rewrite !(coefD, coefMX, coef_map) /= linearD /= !coefC. by rewrite !(fun_if D) linear0. rewrite derivMXaddC !hornerE mulrDl mulrAC addrAC linearD /=; congr (_ + _). by rewrite addrCA -mulrDl -IHp // addrC (Derivation_mul derD) ?rpred_horner. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)