proposition: Lemma normalClosureP E F K' : (E <= K')%VS -> (F <= K')%VS -> normalField E K' -> (normalClosure E F <= K')%VS.
proof: Proof. move=> EK' FK' /'forall_implyP/(_ _ _)/eqP/= sK'. apply/big_prod_subfieldP => /= u uEF; rewrite rpred_prod// => s s_end. by apply/subvP: (uEF s s_end); rewrite -(sK' _ s_end) limgS// prodv_sub. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)