proposition: Lemma Gauss_gcdr p m n : coprime p m -> gcdn p (m * n) = gcdn p n.
proof: Proof. move=> co_pm; apply/eqP; rewrite eqn_dvd !dvdn_gcd !dvdn_gcdl /=. rewrite andbC dvdn_mull ?dvdn_gcdr //= -(@Gauss_dvdr _ m) ?dvdn_gcdr //. by rewrite /coprime gcdnAC (eqnP co_pm) gcd1n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)