proposition: Lemma module_baseVspace M0 : (F1 * M0 <= M0)%VS -> {V | M0 = baseVspace V & M0 =i V}.
proof: Proof. move=> modM0; pose V := <<vbasis (vspaceOver F1 M0) : seq L>>%VS. suffices memM0: M0 =i V. by exists V => //; apply/vspaceP=> v; rewrite mem_baseVspace memM0. move=> v; rewrite -{1}(field_module_eq modM0) -(mem_vspaceOver M0) {}/V. move: (vspaceOver F1 M0) => M. apply/idP/idP=> [/coord_vbasis|/coord_span]->; apply/memv_suml=> i _. rewrite /(_ *: _) /= /fieldOver_scale; case: (coord _ i _) => /= x. rewrite {1}F1unlock mem_baseVspace => /vlineP[{}x ->]. by rewrite -(@scalerAl F L) mul1r memvZ ?memv_span ?memt_nth. move: (coord _ i _) => x; rewrite -[_`_i]mul1r scalerAl -tnth_nth. have F1x: x%:A \in F1. by rewrite F1unlock mem_baseVspace (@memvZ F L) // mem1v. by congr (_ \in M): (memvZ (Subvs F1x) (vbasis_mem (mem_tnth i _))). 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)