proposition: Lemma uniq_roots_Xn_sub_xn : x != 0 -> uniq ws.
proof: Proof. Proof using w_root. move=> xN0; rewrite /image_mem (map_comp (fun i => x * w ^+ i)) val_enum_ord. apply/(uniqP 0) => i j; rewrite !inE size_map size_iota/= => ip jp. rewrite !(nth_map 0%N) ?size_iota// ?nth_iota// => /(mulfI xN0). by move/eqP; rewrite (eq_prim_root_expr w_root) !modn_small// => /eqP. 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)