proposition: Lemma solvable_prodv (k E F : {subfield L}) : (k <= F)%VS -> solvable_ext k E -> solvable_ext F (E * F)%AS.
proof: Proof. move=> kF /andP[sepkE solkE]; apply/solvable_extP => //. exists ([aspace of normalClosure k E] * F)%AS. rewrite (@galois_prodvr _ _ k) ?normalClosure_galois//. rewrite ?prodvSl ?sub_normalClosure//=. rewrite (isog_sol (galois_isog (normalClosure_galois _) _))//. rewrite (solvableS _ solkE)// galS// subv_cap kF. by rewrite galois_subW ?normalClosure_galois. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)