proposition: Lemma map_galK : {in kAEnd 1 E, map_gal \o gal E =1 gal (iota @: E) \o map_ahom iota }.
proof: Proof. move=> s; rewrite inE kAut1E => sE. apply/eqP/gal_eqP => _/memv_imgP[x xE ->]/=. rewrite map_galE// !galK ?memv_img ?map_ahomE//. by rewrite -limg_comp map_ahomC limg_comp limgS. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)