proposition: Lemma gcdsr_primitive : forall p, exists q, p = (gcdsr p)%:P * q /\ primitive q.
proof: Proof. move=> p; rewrite /primitive. suff H: exists q, p = (gcdsr p)%:P * q. have [-> | p0] := eqVneq p 0; first by exists 1; rewrite gcdsr0 mulr1 gcdsr1. case: H=> x H; exists x; split=> //. rewrite -(@eqd_mul2l _ (gcdsr p)). by rewrite mulr1 {2}H (eqd_trans _ (mulr_gcdsr _ x)). by apply: contraPneq H => ->; apply/eqP; rewrite mul0r. elim/poly_ind: p=> /= [|p c [q IH]]; first by exists 1; rewrite gcdsr0 mul0r. case/dvdrP: (dvdr_gcdr c (gcdsr p))=> wr Hr; rewrite mulrC in Hr. case/dvdrP: (dvdr_gcdl c (gcdsr p))=> wl Hl; rewrite mulrC in Hl. exists (wr%:P * q * 'X + wl%:P). by rewrite mulrDr gcdsr_gcdl !mulrA -!polyCM -Hl -Hr -IH. 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)