proposition: Lemma coprimep_expl k m n : coprimep m n -> coprimep (m ^+ k) n.
proof: Proof. by case: k => [|k] co_pm; rewrite ?coprime1p // coprimep_pexpl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)