proposition: Lemma surj_gal_perm : (gal_perm @* 'Gal (K / 1%AS) = 'Sym_('I_d))%g.
proof: Proof. apply/eqP; rewrite eqEsubset subsetT/=. rewrite -(@gen_tperm_cycle _ i0 i1 (gal_perm gal_cycle)); do ?by rewrite ?dpair_ij0 ?card_ord ?gal_perm_cycle_order. by rewrite gen_subG; apply/subsetP => s /set2P[]->; rewrite -?galJ_tperm ?mem_morphim ?gal1. 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)