proposition: Lemma injm_gal_perm : ('injm gal_perm)%g.
proof: Proof. apply/subsetP => u /mker/= gu1; apply/set1gP/eqP/gal_eqP => x Kx. have fixrp : all (fun r => frel u r r) rp. apply/allP => r/= /(nthP 0)[i]; rewrite size_rp => ltid <-. have /permP/(_ (Ordinal ltid))/(congr1 val)/= := gu1. by rewrite perm1/= => {2}<-; rewrite gal_permP. rewrite K_eq /= in Kx. elim/last_ind: rp x Kx fixrp => [|s r IHs] x. rewrite adjoin_nil subfield_closed => x1 _. by rewrite (fixed_gal _ (gal1 u)) ?sub1v ?gal_id. rewrite adjoin_rcons => /Fadjoin_poly_eq <-. rewrite all_rcons => /andP[/eqP ur /IHs us]. rewrite gal_id -horner_map/= ur map_poly_id//=. move=> a /(nthP 0)[i i_lt <-]; rewrite us ?gal_id//. exact/polyOverP/Fadjoin_polyOver. 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)