proposition: Lemma separable_mulv K x y : separable_element K x -> separable_element K y -> separable_element K (x * y).
proof: Proof. move/(separable_elementS (subv_adjoin K y))=> sepKy_x sepKy. have [z defKz] := Primitive_Element_Theorem x sepKy. have /(adjoin_separableP _): x * y \in <<K; z>>%VS. by rewrite -defKz rpredM ?memv_adjoin // subvP_adjoin ?memv_adjoin. apply; apply: adjoin_separable sepKy (adjoin_separable sepKy_x _). by rewrite defKz base_separable ?memv_adjoin. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)