proposition: Lemma base_vspaceOver V : baseVspace (vspaceOver F V) =i (F * V)%VS.
proof: Proof. by move=> v; rewrite mem_baseVspace mem_vspaceOver. 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)