proposition: Lemma prim_mulX : forall p, primitive p -> primitive (p * 'X).
proof: Proof. rewrite /primitive=> p H; apply: (@eqd_trans _ (gcdsr p) _ 1)=> //. by rewrite -[p * _]addr0 gcdsr_gcdl (eqd_trans (gcd0r _)). 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)