proposition: Lemma char0_galois E F : (E <= F)%VS -> normalField E F -> galois E F.
proof: Proof. by move=> sEF nEF; apply/and3P; split=> //; apply: char0_separable. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra all_field)