proposition: Lemma zprimitive_min p a q : p != 0 -> p = a *: q -> {b | sgz b = sgz (lead_coef q) & q = b *: zprimitive p}.
proof: Proof. move=> nz_p Dp; have /dvdzP/sig_eqW[b Db]: (a %| zcontents p)%Z. by rewrite dvdz_contents; apply/polyOver_dvdzP; exists q. suffices ->: q = b *: zprimitive p. by rewrite lead_coefZ sgzM sgz_lead_primitive nz_p mulr1; exists b. apply: (@mulfI _ a%:P). by apply: contraNneq nz_p; rewrite Dp -mul_polyC => ->; rewrite mul0r. by rewrite !mul_polyC -Dp scalerA mulrC -Db -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)