proposition: Lemma zprimitiveM p q : zprimitive (p * q) = zprimitive p * zprimitive q.
proof: Proof. have [pq_0|] := eqVneq (p * q) 0. rewrite pq_0; move/eqP: pq_0; rewrite mulf_eq0. by case/pred2P=> ->; rewrite !zprimitive0 (mul0r, mulr0). rewrite -zcontents_eq0 -polyC_eq0 => /mulfI; apply; rewrite !mul_polyC. by rewrite -zpolyEprim zcontentsM -scalerA scalerAr scalerAl -!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)