proposition: Lemma normalClosure_id E F : (E <= F)%VS -> normalField E F -> normalClosure E F = F.
proof: Proof. by move=> EF nEF; apply/eqP; rewrite eqEsubv/= normalClosureSr normalClosureP. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)