proposition: Lemma galois_normalW E F : galois E F -> (normalField E F)%VS.
proof: Proof. by case/and3P. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)