proposition: Lemma dvdp_exp d k p : 0 < k -> d %| p -> d %| (p ^+ k).
proof: Proof. by case: k => // k _ d_dv_m; rewrite exprS dvdp_mulr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)