proposition: Lemma dvdp_minpoly_Xn_subn E : (x ^+ p)%R \in E -> minPoly E x %| ('X^p - (x ^+ p)%:P).
proof: Proof. Proof using. move=> xpE; have [->|p_gt0] := posnP p; first by rewrite !expr0 subrr dvdp0. by rewrite minPoly_dvdp /root ?poly_XnsubC_over// !hornerE ?hornerXn subrr. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field polyrcf) Abel(various classic_ext map_gal algR) Abel(char0 cyclotomic_ext real_closed_ext)