proposition: Lemma pnat_coprime pi m n : pi.-nat m -> pi^'.-nat n -> coprime m n.
proof: Proof. case/andP=> m_gt0 pi_m /andP[n_gt0 pi'_n]; rewrite coprime_has_primes //. by apply/hasPn=> p /(allP pi'_n); apply/contra/allP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)