proposition: Lemma normalField_cast_eq x : x \in 'Gal(E / K) -> {in M, normalField_cast x =1 x}.
proof: Proof. have [sKM sME] := andP sKME; have sKE := subv_trans sKM sME. rewrite gal_kAut // => /(normalField_kAut sKME nKM). by rewrite kAutE => /andP[_ /galK]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)