proposition: Lemma normal_prodvr (k K F : {subfield L}) : (k <= K)%VS -> (k <= F)%VS -> normalField k K -> normalField F (K * F).
proof: Proof. move=> kK kF /(splitting_normalField kK) [p pk [rs p_eq krs]]. apply/splitting_normalField; rewrite ?field_subvMl//; exists p. by apply: polyOverS pk => x; apply: subvP. exists rs => //; apply/eqP; rewrite eqEsubv; apply/andP; split. apply/Fadjoin_seqP; rewrite field_subvMl; split => //= r rrs. by apply: (subvP (field_subvMr _ _)); rewrite -krs seqv_sub_adjoin. apply/prodvP => x y xK yF; rewrite rpredM//; last first. by rewrite (subvP (subv_adjoin_seq _ _))//. by rewrite -krs in xK; apply: subvP xK; apply: adjoin_seqSl. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)