proposition: Lemma p'natE p n : prime p -> p^'.-nat n = ~~ (p %| n).
proof: Proof. case: n => [|n] p_pr; first by case: p p_pr. by rewrite p'natEpi // mem_primes p_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)