proposition: Fact extendDerivation_scalable_subproof E (adjEx := Fadjoin_poly E x) : let body y (p := adjEx y) := (map_poly D p).[x] + p^`().[x] * Dx E in scalable body.
proof: Proof. move: Dx => C /= a u. rewrite /adjEx linearZ /= -mul_polyC derivM derivC mul0r add0r -/adjEx. rewrite !hornerE /= -scalerAl mul1r raddfD /=. have ->: map_poly D (a%:A%:P * adjEx u) = a%:A%:P * map_poly D (adjEx u). apply/polyP=> i; rewrite !mul_polyC !coef_map !coefZ !mulr_algl /= linearZ. by rewrite coef_map. by rewrite !hornerE !mulr_algl -scalerAl. 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)