proposition: Lemma irreducible_exp n (p q : {poly R}) : irreducible_poly p -> 0 < n -> p %| q ^+ n = (p %| q).
proof: Proof. move=> pI. elim: n => // [] [|n] // /(_ isT) IH _. apply/idP/idP; rewrite exprS; last first. by move=> /dvdp_trans; apply; apply: dvdp_mulr. have [pCq|pNCq] := boolP (coprimep p q); first by rewrite Gauss_dvdpr // IH. have /(irredp_XsubCP pI)[pCq|/andP[_ pDg] _] : gcdp p q %| p. - by rewrite dvdp_gcdl. - by case/negP: pNCq; rewrite /coprimep size_poly_eq1. by apply: dvdp_trans pDg (dvdp_gcdr _ _). Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)