proposition: Lemma rdvdp_comp_poly (r p q : {poly R}) : p \is monic -> r \is monic -> r != 1 -> rdvdp p q -> rdvdp (p \Po r) (q \Po r).
proof: Proof. move=> pM rM rD1 /rdvdpP => /(_ pM) [qq qqE]. apply/rdvdpP; first by apply: monic_comp_poly. by exists (qq \Po r); rewrite qqE comp_polyM. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)