proposition: Lemma gcdsr_gcdl : forall p c, gcdsr (p * 'X + c%:P) = gcdr c (gcdsr p).
proof: Proof. move=> p c. have [-> | p0] := eqVneq p 0. rewrite mul0r add0r gcdsr0 /gcdsr polyseqC. by case: eqP => //= ->; apply/eqP; rewrite eq_sym gcdr_eq0 eqxx. by rewrite -cons_poly_def polyseq_cons /nilp size_poly_eq0 p0. 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)