proposition: Lemma zprimitive_irr p a q : p != 0 -> zprimitive p = a *: q -> a = sgz (lead_coef q).
proof: Proof. move=> nz_p Dp; have: p = (a * zcontents p) *: q. by rewrite mulrC -scalerA -Dp -zpolyEprim. case/zprimitive_min=> // b <- /eqP. rewrite Dp -{1}[q]scale1r scalerA -subr_eq0 -scalerBl scale_poly_eq0 subr_eq0. have{Dp} /negPf->: q != 0. by apply: contraNneq nz_p; rewrite -zprimitive_eq0 Dp => ->; rewrite scaler0. by case: b a => [[|[|b]] | [|b]] [[|[|a]] | [|a]] //; rewrite mulr0. 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)