proposition: Lemma zcontentsZ a p : zcontents (a *: p) = a * zcontents p.
proof: Proof. have [-> | nz_a] := eqVneq a 0; first by rewrite scale0r mul0r zcontents0. rewrite {2}[a]intEsg mulrCA -mulrA -PoszM big_distrr /= mulrCA mulrA -sgzM. rewrite -lead_coefZ; congr (_ * _%:Z); rewrite size_scale //. by apply: eq_bigr => i _; rewrite coefZ abszM. 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)