proposition: Lemma gcdp_comp_poly r p q : gcdp p q \Po r %= gcdp (p \Po r) (q \Po r).
proof: Proof. apply/andP; split. by rewrite dvdp_gcd !dvdp_comp_poly ?dvdp_gcdl ?dvdp_gcdr. case: (Bezoutp p q) => [[u v]] /andP []. move/(dvdp_comp_poly r) => Huv _. rewrite (dvdp_trans _ Huv) // comp_polyD !comp_polyM. by rewrite dvdp_add // dvdp_mull // (dvdp_gcdl,dvdp_gcdr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)