proposition: Lemma integral_poly (p : {poly K}) : (forall i, integralOver RtoK p`_i) <-> {in p : seq K, integralRange RtoK}.
proof: Proof. split=> intRp => [_ /(nthP 0)[i _ <-] // | i]; rewrite -[p]coefK coef_poly. by case: ifP => [ltip | _]; [apply/intRp/mem_nth | apply: integral0]. 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)