proposition: Lemma sgz_contents p : sgz (zcontents p) = sgz (lead_coef p).
proof: Proof. rewrite /zcontents mulrC sgzM sgz_id; set d := _%:Z. have [-> | nz_p] := eqVneq p 0; first by rewrite lead_coef0 mulr0. rewrite gtr0_sgz ?mul1r // ltz_nat polySpred ?big_ord_recr //= -lead_coefE. by rewrite gcdn_gt0 orbC absz_gt0 lead_coef_eq0 nz_p. 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)