proposition: Lemma gcdp_mul2l p q r : gcdp (p * q) (p * r) %= (p * gcdp q r).
proof: Proof. have [->|hp] := eqVneq p 0; first by rewrite !mul0r gcdp0 eqpxx. rewrite /eqp !dvdp_gcd !dvdp_mul2l // dvdp_gcdr dvdp_gcdl !andbT. move: (Bezoutp q r) => [[u v]] huv. rewrite eqp_sym in huv; rewrite (eqp_dvdr _ (eqp_mull _ huv)). rewrite mulrDr ![p * (_ * _)]mulrCA. by apply: dvdp_add; rewrite dvdp_mull// (dvdp_gcdr, dvdp_gcdl). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)