proposition: Lemma separable_add 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 rpredD ?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(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset prime) mathcomp(binomial ssralg poly polydiv fingroup perm) mathcomp(morphism quotient gproduct finalg zmodp cyclic) mathcomp(matrix mxalgebra mxpoly polyXY vector falgebra) mathcomp(fieldext)