proposition: Lemma zprimitiveZ a p : a != 0 -> zprimitive (a *: p) = zprimitive p.
proof: Proof. have [-> | nz_p nz_a] := eqVneq p 0; first by rewrite scaler0. apply: (@mulfI _ (a * zcontents p)%:P). by rewrite polyC_eq0 mulf_neq0 ?zcontents_eq0. by rewrite -{1}zcontentsZ !mul_polyC -zpolyEprim -scalerA -zpolyEprim. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)