proposition: Lemma gal_perm_eq (g : gal_of K) : perm_eq [seq g x | x <- trp] trp.
proof: Proof. apply: prod_XsubC_eq; apply/eqP; rewrite -eqp_monic ?monic_prod_XsubC//. rewrite -(eqp_rtrans ratr_p) big_map. apply: (@eqp_trans _ (map_poly (g \o ratr) p)); last first. apply/eqpW/eq_map_poly => x /=; rewrite (fixed_gal _ (gal1 g)) ?sub1v//. by rewrite -alg_num_field rpredZ ?mem1v. rewrite map_poly_comp/=; have := ratr_p; rewrite -(eqp_map g)/=. move=> /eqp_rtrans/=->; apply/eqpW; rewrite rmorph_prod /=. by apply: eq_bigr => x; rewrite rmorphB/= map_polyX map_polyC/=. 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)