proposition: Lemma separable_prodvr (k K F : {subfield L}) : (k <= F)%VS -> separable k K -> separable F (K * F).
proof: Proof. by move=> kF sepkK; rewrite separable_prodv separable_refl (separableSl kF). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)