proposition: Lemma separableS K1 K2 E2 E1 : (K1 <= K2)%VS -> (E2 <= E1)%VS -> separable K1 E1 -> separable K2 E2.
proof: Proof. move=> sK12 /subvP sE21 /separableP sepK1_E1. by apply/separableP=> y /sE21/sepK1_E1/(separable_elementS sK12). 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)