proposition: Lemma gcdsr_odivp : forall p, p != 0 -> exists x, p %/? (gcdsr p)%:P = Some (x : {poly R}) /\ primitive x.
proof: Proof. move=> p p0; case: (gcdsr_primitive p)=> x [Hp primx]. exists x; split=> //. rewrite {1}Hp odivr_mulKr //. by apply: contraPneq Hp => ->; apply/eqP; rewrite mul0r. 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)