proposition: Lemma normalField_kAut K M E f : (K <= M <= E)%VS -> normalField K M -> kAut K E f -> kAut K M f.
proof: Proof. case/andP=> sKM sME nKM /kAut_to_gal[x galEx /(sub_in1 (subvP sME))Df]. have sKE := subv_trans sKM sME; rewrite gal_kHom // in galEx. rewrite (kAut_eq sKM Df) /kAut (kHomSr sME) //= (forall_inP nKM) // inE. by rewrite kAutfE; apply/kAHomP; apply: (kAHomP galEx). 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)