proposition: Lemma Gauss_dvdpl p q d: coprimep d q -> (d %| p * q) = (d %| p).
proof: Proof. move/Bezout_coprimepP=>[[u v] Puv]; apply/idP/idP; last exact: dvdp_mulr. move/(eqp_mull p): Puv; rewrite mulr1 mulrDr eqp_sym=> peq dpq. rewrite (eqp_dvdr _ peq) dvdp_addr; first by rewrite mulrA mulrAC dvdp_mulr. by rewrite mulrA dvdp_mull ?dvdpp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)