proposition: Lemma galois_prodvr (k K F : {subfield L}) : (k <= F)%VS -> galois k K -> galois F (K * F).
proof: Proof. move=> kF /and3P[kK sep norm]; rewrite /galois field_subvMl/=. by rewrite (separable_prodvr kF)// (normal_prodvr kK kF). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)