proposition: Lemma dvdp_mull m d n : d %| n -> d %| m * n.
proof: Proof. case: (eqVneq d 0) => [-> /dvd0pP -> | dn0]; first by rewrite mulr0 dvdpp. rewrite dvdp_eq => /eqP e. apply: (@eq_dvdp (lead_coef d ^+ scalp n d) (m * (n %/ d))). by rewrite expf_neq0 // lead_coef_eq0. by rewrite scalerAr e mulrA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)