proposition: Lemma separable_Fadjoin_seq K rs : all (separable_element K) rs -> separable K <<K & rs>>.
proof: Proof. elim/last_ind: rs => [|s x IHs] in K *. by rewrite adjoin_nil subfield_closed separable_refl. rewrite all_rcons adjoin_rcons => /andP[sepKx /IHs/separable_trans-> //]. by rewrite -adjoin_separable_eq (separable_elementS _ sepKx) ?subv_adjoin_seq. 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)