proposition: Lemma capv_galois (k K F : {subfield L}) : (k <= F)%VS -> galois k K -> galois (K :&: F) K.
proof: Proof. move=> kF /splitting_galoisField [p [pk p_sep [rs p_eq krs]]]. have k_subKF: (k <= K :&: F)%VS. apply/subvP => x xk. by rewrite memv_cap (subvP kF)// -krs (subvP (subv_adjoin_seq _ _)). apply/splitting_galoisField; exists p; split => //. by apply: polyOverS pk; apply/subvP. exists rs => //; apply/eqP; rewrite -krs eqEsubv andbC adjoin_seqSl//=. by apply/Fadjoin_seqP; split; [rewrite /= krs capvSl|apply: seqv_sub_adjoin]. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)