proposition: Lemma integral_root p u : p != 0 -> root p u -> {in p : seq E, integralRange FtoE} -> integralOver FtoE u.
proof: Proof. move=> nz_p pu0 algFp. have mon_p1: mk_mon p \is monic. by rewrite monicE lead_coefZ mulVf ?lead_coef_eq0. have p1u0: root (mk_mon p) u by rewrite rootE hornerZ (rootP pu0) mulr0. apply: integral_root_monic mon_p1 p1u0 _ => _ /(nthP 0)[i ltip <-]. rewrite coefZ mulrC; rewrite size_scale ?invr_eq0 ?lead_coef_eq0 // in ltip. by apply: integral_div; apply/algFp/mem_nth; rewrite -?polySpred. 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)