proposition: Lemma gcdsr_mull : forall a p, gcdsr (a%:P * p) %= a * gcdsr p.
proof: Proof. move=> a. elim/poly_ind=> [|p c IH]; first by rewrite mulr0 gcdsr0 mulr0. rewrite mulrDr -polyCM mulrA [X in X %= _]gcdsr_gcdl. rewrite (eqd_trans (eqd_gcd (eqdd _) IH)) //. by rewrite (eqd_trans (gcdr_mul2l _ _ _)) // -gcdsr_gcdl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(path choice fintype tuple finset ssralg) mathcomp(matrix poly) mathcomp(bigop polydiv) CoqEAL(stronglydiscrete dvdring)