proposition: Lemma dvdp_exp_XsubC (R : idomainType) (p : {poly R}) (c : R) n : reflect (exists2 k, (k <= n)%N & p %= ('X - c%:P) ^+ k) (p %| ('X - c%:P) ^+ n).
proof: Proof. apply: (iffP idP) => [|[k lkn /eqp_dvdl->]]; last by rewrite dvdp_exp2l. move=> /Pdiv.WeakIdomain.dvdpP[[/= a q] a_neq0]. have [m [r]] := multiplicity_XsubC p c; have [->|pN0]/= := eqVneq p 0. rewrite mulr0 => _ _ /eqP; rewrite scale_poly_eq0 (negPf a_neq0)/=. by rewrite expf_eq0/= andbC polyXsubC_eq0. move=> rNc ->; rewrite mulrA => eq_qrm; exists m. have: ('X - c%:P) ^+ m %| a *: ('X - c%:P) ^+ n by rewrite eq_qrm dvdp_mull. by rewrite (eqp_dvdr _ (eqp_scale _ _))// dvdp_Pexp2l// size_XsubC. suff /eqP : size r = 1%N. by rewrite size_poly_eq1 => /eqp_mulr/eqp_trans->//; rewrite mul1r eqpxx. have : r %| a *: ('X - c%:P) ^+ n by rewrite eq_qrm mulrAC dvdp_mull. rewrite (eqp_dvdr _ (eqp_scale _ _))//. move: rNc; rewrite -coprimep_XsubC => /(coprimep_expr n) /coprimepP. by move=> /(_ _ (dvdpp _)); rewrite -size_poly_eq1 => /(_ _)/eqP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)