proposition: Lemma dvdp_pexp2r m n k : k > 0 -> (m ^+ k %| n ^+ k) = (m %| n).
proof: Proof. move=> k_gt0; apply/idP/idP; last exact: dvdp_exp2r. have [-> // | nn0] := eqVneq n 0; have [-> | mn0] := eqVneq m 0. move/prednK: k_gt0=> {1}<-; rewrite exprS mul0r //= !dvd0p expf_eq0. by case/andP=> _ ->. set d := gcdp m n; have := dvdp_gcdr m n; rewrite -/d dvdp_eq. set c1 := _ ^+ _; set n' := _ %/ _; move/eqP=> def_n. have := dvdp_gcdl m n; rewrite -/d dvdp_eq. set c2 := _ ^+ _; set m' := _ %/ _; move/eqP=> def_m. have dn0 : d != 0 by rewrite gcdp_eq0 negb_and nn0 orbT. have c1n0 : c1 != 0 by rewrite !expf_neq0 // lead_coef_eq0. have c2n0 : c2 != 0 by rewrite !expf_neq0 // lead_coef_eq0. have c2k_n0 : c2 ^+ k != 0 by rewrite !expf_neq0 // lead_coef_eq0. rewrite -(@dvdpZr (c1 ^+ k)) ?expf_neq0 ?lead_coef_eq0 //. rewrite -(@dvdpZl (c2 ^+ k)) // -!exprZn def_m def_n !exprMn. rewrite dvdp_mul2r ?expf_neq0 //. have: coprimep (m' ^+ k) (n' ^+ k). by rewrite coprimep_pexpl // coprimep_pexpr // coprimep_div_gcd ?mn0. move/coprimepP=> hc hd. have /size_poly1P [c cn0 em'] : size m' == 1. case: (eqVneq m' 0) def_m => [-> /eqP | m'_n0 def_m]. by rewrite mul0r scale_poly_eq0 (negPf mn0) (negPf c2n0). have := hc _ (dvdpp _) hd; rewrite -size_poly_eq1. rewrite polySpred; last by rewrite expf_eq0 negb_and m'_n0 orbT. by rewrite size_exp eqSS muln_eq0 orbC eqn0Ngt k_gt0 /= -eqSS -polySpred. rewrite -(@dvdpZl c2) // def_m em' mul_polyC dvdpZl //. by rewrite -(@dvdpZr c1) // def_n dvdp_mull. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)