proposition: Lemma polyOver_dvdzP a p : reflect (exists q, p = a *: q) (p \is a polyOver (dvdz a)).
proof: Proof. apply: (iffP idP) => [/map_poly_divzK | [q ->]]. by exists (map_poly (divz^~ a) p). by apply/polyOverP=> i; rewrite coefZ dvdz_mulr. 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)