proposition: Lemma dvdp_comp_poly r p q : (p %| q) -> (p \Po r) %| (q \Po r).
proof: Proof. have [-> | pn0] := eqVneq p 0. by rewrite comp_poly0 !dvd0p; move/eqP->; rewrite comp_poly0. rewrite dvdp_eq; set c := _ ^+ _; set s := _ %/ _; move/eqP=> Hq. apply: (@eq_dvdp c (s \Po r)); first by rewrite expf_neq0 // lead_coef_eq0. by rewrite -comp_polyZ Hq comp_polyM. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)