fact: Definition zcontents (p : {poly int}) : int := sgz (lead_coef p) * \big[gcdn/0]_(i < size p) `|(p`_i)%R|%N.
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)