proposition: Lemma coprime_pexpl k m n : 0 < k -> coprime (m ^ k) n = coprime m n.
proof: Proof. case: k => // k _; elim: k => [|k IHk]; first by rewrite expn1. by rewrite expnS coprimeMl -IHk; case coprime. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)