proposition: Lemma coprime_pi' m n : m > 0 -> n > 0 -> coprime m n = \pi(m)^'.-nat n.
proof: Proof. by move=> m_gt0 n_gt0; rewrite /pnat n_gt0 all_predC coprime_has_primes. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)