proposition: Lemma Euclid_dvdX m n p : prime p -> (p %| m ^ n) = (p %| m) && (n > 0).
proof: Proof. case: n => [|n] pr_p; first by rewrite andbF Euclid_dvd1. by apply: (inv_inj negbK); rewrite !andbT -!prime_coprime // coprime_pexpr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)