proposition: Lemma primesX m n : n > 0 -> primes (m ^ n) = primes m.
proof: Proof. case: n => // n _; rewrite expnS; have [-> // | m_gt0] := posnP m. apply/eq_primes => /= p; elim: n => [|n IHn]; first by rewrite muln1. by rewrite primesM ?(expn_gt0, expnS, IHn, orbb, m_gt0). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)