proposition: Lemma gcdr_gcdsr_muladdr : forall a p q, gcdr a (gcdsr (a%:P * p + q)) %= gcdr a (gcdsr q).
proof: Proof. move=> a. elim/poly_ind=> [|p c IH q]; first by move=> q; rewrite mulr0 add0r eqdd. rewrite mulrDr mulrA -polyCM addrC addrA -[q]polyseqK. case: q=> /= q _; case: q=> /= [|d p1]. rewrite add0r gcdsr_gcdl (eqd_trans (gcdrA a _ _)) // -[a*c]addr0. rewrite (eqd_trans (eqd_gcd (gcdr_addl_mul a 0 c) (eqdd _))) //. by rewrite (eqd_trans (eqd_gcd (gcdr0 a) (eqdd _))) // -[_ * p]addr0 (IH 0). rewrite cons_poly_def -!addrA [d%:P + _]addrCA -polyCD addrA -mulrDl. rewrite !gcdsr_gcdl [Poly p1 + _]addrC [d+_]addrC (eqd_trans (gcdrA _ _ _)) //. rewrite (eqd_trans ((eqd_gcd (gcdr_addl_mul a d c)) (eqdd _))) //. rewrite (eqd_trans (gcdrAC _ _ _)) ?(eqd_trans (eqd_gcd (IH _) (eqdd d))) //. rewrite (eqd_trans (gcdrAC _ _ _)) // eqd_sym (eqd_trans (gcdrA _ _ _)) //. 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)