proposition: Lemma coprime_has_primes m n : 0 < m -> 0 < n -> coprime m n = ~~ has [in primes m] (primes n).
proof: Proof. move=> m_gt0 n_gt0; apply/eqP/hasPn=> [mn1 p | no_p_mn]. rewrite /= !mem_primes m_gt0 n_gt0 /= => /andP[pr_p p_n]. have:= prime_gt1 pr_p; rewrite pr_p ltnNge -mn1 /=; apply: contra => p_m. by rewrite dvdn_leq ?gcdn_gt0 ?m_gt0 // dvdn_gcd ?p_m. apply/eqP; rewrite eqn_leq gcdn_gt0 m_gt0 andbT leqNgt; apply/negP. move/pdiv_prime; set p := pdiv _ => pr_p. move/implyP: (no_p_mn p); rewrite /= !mem_primes m_gt0 n_gt0 pr_p /=. by rewrite !(dvdn_trans (pdiv_dvd _)) // (dvdn_gcdl, dvdn_gcdr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)