proposition: Lemma integral_horner (p : {poly K}) u : {in p : seq K, integralRange RtoK} -> integralOver RtoK u -> integralOver RtoK p.[u].
proof: Proof. by move=> ? /integral_opp/intR_XsubC/integral_horner_root; apply. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)