proposition: Lemma root_dvdp (F : idomainType) (p q : {poly F}) (x : F) : root p x -> p %| q -> root q x.
proof: Proof. rewrite -!dvdp_XsubCl; exact: dvdp_trans. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)