proposition: Lemma dvdp_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.
proof: Proof. case: (eqVneq d1 0) => [-> /dvd0pP -> | d1n0]; first by rewrite !mul0r dvdpp. case: (eqVneq d2 0) => [-> _ /dvd0pP -> | d2n0]; first by rewrite !mulr0. rewrite dvdp_eq; set c1 := _ ^+ _; set q1 := _ %/ _; move/eqP=> Hq1. rewrite dvdp_eq; set c2 := _ ^+ _; set q2 := _ %/ _; move/eqP=> Hq2. apply: (@eq_dvdp (c1 * c2) (q1 * q2)). by rewrite mulf_neq0 // expf_neq0 // lead_coef_eq0. rewrite -scalerA scalerAr scalerAl Hq1 Hq2 -!mulrA. by rewrite [d1 * (q2 * _)]mulrCA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)