proposition: Lemma dvdp_exp2r p q k : p %| q -> p ^+ k %| q ^+ k.
proof: Proof. case: (eqVneq p 0) => [-> /dvd0pP -> // | pn0]. rewrite dvdp_eq; set c := _ ^+ _; set t := _ %/ _; move/eqP=> e. apply: (@eq_dvdp (c ^+ k) (t ^+ k)); first by rewrite !expf_neq0 ?lead_coef_eq0. by rewrite -exprMn -exprZn; congr (_ ^+ k). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)