proposition: Lemma Gauss_dvdp m n p : coprimep m n -> (m * n %| p) = (m %| p) && (n %| p).
proof: Proof. have [-> | mn0] := eqVneq m 0. by rewrite coprime0p => /eqp_dvdl->; rewrite !mul0r dvd0p dvd1p andbT. have [-> | nn0] := eqVneq n 0. by rewrite coprimep0 => /eqp_dvdl->; rewrite !mulr0 dvd1p. move=> hc; apply/idP/idP => [mnmp | /andP [dmp dnp]]. move/Gauss_dvdpl: hc => <-; move: (dvdp_mull m mnmp); rewrite dvdp_mul2l //. move->; move: (dvdp_mulr n mnmp); rewrite dvdp_mul2r // andbT. exact: dvdp_mulr. move: (dnp); rewrite dvdp_eq. set c2 := _ ^+ _; set q2 := _ %/ _; move/eqP=> e2. have/esym := Gauss_dvdpl q2 hc; rewrite -e2. have -> : m %| c2 *: p by rewrite -mul_polyC dvdp_mull. rewrite dvdp_eq; set c3 := _ ^+ _; set q3 := _ %/ _; move/eqP=> e3. apply: (@eq_dvdp (c3 * c2) q3). by rewrite mulf_neq0 // expf_neq0 // lead_coef_eq0. by rewrite mulrA -e3 -scalerAl -e2 scalerA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)