proposition: Lemma map_gal_inj : ('injm map_gal)%g.
proof: Proof. apply/injmP => /= f g _ _ eq_fg; apply/eqP/gal_eqP => x xE. have /eqP/gal_eqP/(_ _ (memv_img iota xE)) := eq_fg. by rewrite !map_galE// => /fmorph_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)