proposition: Lemma pnatX pi m n : pi.-nat (m ^ n) = pi.-nat m || (n == 0).
proof: Proof. by case: n => [|n]; rewrite orbC // /pnat expn_gt0 orbC primesX. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)