proposition: Lemma eqp_gcdr p q r : q %= r -> gcdp p q %= gcdp p r.
proof: Proof. move=> eqr; rewrite /eqp !(dvdp_gcd, dvdp_gcdl, andbT) /=. by rewrite -(eqp_dvdr _ eqr) dvdp_gcdr (eqp_dvdr _ eqr) dvdp_gcdr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)