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