proposition: Lemma Xn_sub_xnE : (n > 0)%N -> 'X^n - (x ^+ n)%:P = \prod_(i < n) ('X - (x * w ^+ i)%:P).
proof: Proof. Proof using w_root. move=> n_gt0; have [->|xN0] := eqVneq x 0. under eq_bigr do rewrite mul0r subr0. by rewrite expr0n gtn_eqF// subr0 prodr_const card_ord. rewrite [LHS](@all_roots_prod_XsubC _ _ ws). - by rewrite (monicP _) ?monic_XnsubC// scale1r big_map big_enum. - by rewrite size_XnsubC// size_map size_enum_ord. - rewrite all_map; apply/allP => i _ /=; rewrite /root !hornerE ?hornerXn. by rewrite exprMn exprAC [w ^+ _]prim_expr_order// expr1n mulr1 subrr. - by rewrite uniq_rootsE uniq_roots_Xn_sub_xn. 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)