proposition: Lemma minPolyS K E a : (K <= E)%VS -> minPoly E a %| minPoly K a.
proof: Proof. move=> sKE; apply: minPoly_dvdp; last exact: root_minPoly. by apply: (polyOverSv sKE); rewrite minPolyOver. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)