proposition: Lemma Gauss_gcdpr p m n : coprimep p m -> gcdp p (m * n) %= gcdp p n.
proof: Proof. move=> co_pm; apply/eqP; rewrite /eqp !dvdp_gcd !dvdp_gcdl /= andbC. rewrite dvdp_mull ?dvdp_gcdr // -(@Gauss_dvdpl _ m). by rewrite mulrC dvdp_gcdr. apply/coprimepP=> d; rewrite dvdp_gcd; case/andP=> hdp _ hdm. by move/coprimepP: co_pm; apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)