proposition: Lemma normal_prodv (k K1 K2 : {subfield L}) : normalField k K1 -> normalField k K2 -> normalField k (K1 * K2).
proof: Proof. move=> /'forall_implyP/(_ _ _)/eqP endK1 /'forall_implyP/(_ _ _)/eqP endK2. by apply/'forall_implyP => s s_end; rewrite aimgM endK1// endK2. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)