proposition: Lemma separable_exp (F : finFieldType) n (p q : {poly F}) : separable_poly p -> 0 < n -> p %| q ^+ n = (p %| q).
proof: Proof. case: n => // n pS _. apply/idP/idP; last first. by rewrite exprS => /dvdp_trans; apply; apply: dvdp_mulr. elim: {p}_.+1 {-2}p (ltnSn (size p)) pS => // k IH p SpLk pS pDqn. have [|Sp_gt1] := leqP (size p) 1. rewrite leq_eqVlt => /orP[]. rewrite size_poly_eq1 => /andP[/dvdp_trans-> //]. by apply: dvd1p. rewrite ltnS leqn0 size_poly_eq0 => /eqP pZ. by move: pDqn; rewrite pZ dvd0p expf_eq0 //= => /eqP->. have [r rI rDq] := irreducible_dvdp Sp_gt1. have /dvdpP[s pE] := rDq. have sDp : s %| p by rewrite pE dvdp_mulr. have rCs : coprimep s r by apply: separable_coprime pS _; rewrite -pE. rewrite pE Gauss_dvdp //; apply/andP; split; last first. by rewrite -(@irreducible_exp _ n.+1) // (dvdp_trans _ pDqn). apply: IH; last 2 first. - by apply: dvdp_separable pS; rewrite pE dvdp_mulr. - by rewrite (dvdp_trans _ pDqn). rewrite -(ltn_add2r (size r)) -[(_ + size _)%N]prednK; last first. by case: rI; case: size => // k1; rewrite addnS. rewrite -size_mul; last by apply: irredp_neq0. rewrite -pE (leq_trans _ (_ : (k + 2 <= _))) //. by rewrite !addnS addn0 ltnS. by rewrite leq_add2l; case: rI. apply: separable_poly_neq0. by apply: dvdp_separable pS; rewrite pE dvdp_mulr. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)