proposition: Lemma gcdp_addl_mul p q r: gcdp r (p * r + q) %= gcdp r q.
proof: Proof. suff h m n d : gcdp d n %| gcdp d (m * d + n). apply/andP; split => //. by rewrite {2}(_: q = (-p) * r + (p * r + q)) ?H // mulNr addKr. by rewrite dvdp_gcd dvdp_gcdl /= dvdp_addr ?dvdp_gcdr ?dvdp_mull ?dvdp_gcdl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)