proposition: Lemma Gauss_dvdpr p q d: coprimep d q -> (d %| q * p) = (d %| p).
proof: Proof. by rewrite mulrC; apply: Gauss_dvdpl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)