proposition: Lemma mem_aspaceOver E : (F <= E)%VS -> vspaceOver E =i E.
proof: Proof. by move=> sFE y; rewrite mem_vspaceOver field_module_eq ?sup_field_module. 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)