proposition: Lemma zcontentsM p q : zcontents (p * q) = zcontents p * zcontents q.
proof: Proof. have [-> | nz_p] := eqVneq p 0; first by rewrite !(mul0r, zcontents0). have [-> | nz_q] := eqVneq q 0; first by rewrite !(mulr0, zcontents0). rewrite -[zcontents q]mulr1 {1}[p]zpolyEprim {1}[q]zpolyEprim. rewrite -scalerAl -scalerAr !zcontentsZ; congr (_ * (_ * _)). rewrite [zcontents _]intEsg sgz_contents lead_coefM sgzM !sgz_lead_primitive. apply/eqP; rewrite nz_p nz_q !mul1r [_ == _]eqn_leq absz_gt0 zcontents_eq0. rewrite mulf_neq0 ?zprimitive_eq0 // andbT leqNgt. apply/negP=> /pdivP[r r_pr r_dv_d]; pose to_r : int -> 'F_r := intr. have nz_prim_r q1: q1 != 0 -> map_poly to_r (zprimitive q1) != 0. move=> nz_q1; apply: contraTneq (prime_gt1 r_pr) => r_dv_q1. rewrite -leqNgt dvdn_leq // -(dvdzE r true) -nz_q1 -zcontents_primitive. rewrite dvdz_contents; apply/polyOverP=> i /=; rewrite dvdzE /=. have /polyP/(_ i)/eqP := r_dv_q1; rewrite coef_map coef0 /=. rewrite {1}[_`_i]intEsign rmorphM /= rmorph_sign /= mulf_eq0 signr_eq0 /=. by rewrite -val_eqE /= val_Fp_nat. suffices{nz_prim_r} /idPn[]: map_poly to_r (zprimitive p * zprimitive q) == 0. by rewrite rmorphM mulf_neq0 ?nz_prim_r. rewrite [_ * _]zpolyEprim [zcontents _]intEsign mulrC -scalerA map_polyZ /=. by rewrite scale_poly_eq0 -val_eqE /= val_Fp_nat ?(eqnP r_dv_d). 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)