proposition: Lemma integral_rmorph x : integralOver BtoR x -> integralOver (RtoK \o BtoR) (RtoK x).
proof: Proof. by case=> p; exists p; rewrite // map_poly_comp rmorph_root. 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)