proposition: Lemma coprimeMr p m n : coprime p (m * n) = coprime p m && coprime p n.
proof: Proof. case co_pm: (coprime p m) => /=; first by rewrite /coprime Gauss_gcdr. apply/eqP=> co_p_mn; case/eqnP: co_pm; apply gcdn_def => // d dv_dp dv_dm. by rewrite -co_p_mn dvdn_gcd dv_dp dvdn_mulr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)