proposition: Lemma gal_perm_is_morphism : {in ('Gal(K / 1%AS))%G &, {morph gal_perm : x y / (x * y)%g >-> (x * y)%g}}.
proof: Proof. move=> u v _ _; apply/permP => i; apply/val_inj. apply: (uniqP 0 rp_uniq); rewrite ?inE ?size_rp ?ltn_ord//=. by rewrite permM !gal_permP galM// ?rpK. 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)