proposition: Lemma sup_field_module F E : (F * E <= E)%VS = (F <= E)%VS.
proof: Proof. apply/idP/idP; first exact: subv_trans (field_subvMr F E). by move/(prodvSl E)/subv_trans->; rewrite ?asubv. 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)