proposition: Lemma monic_monic_from_neq0 (F : fieldType) (p : {poly F}) : (p != 0)%B -> (lead_coef p) ^-1 *: p \is monic.
proof: Proof. by move=> ?; rewrite monicE lead_coefZ mulVf ?lead_coef_eq0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)