proposition: Lemma vspaceOverP V_F : {V | [/\ V_F = vspaceOver V, (F * V <= V)%VS & V_F =i V]}.
proof: Proof. pose V := (F * <<vbasis V_F : seq L>>)%VS. have idV: (F * V)%VS = V by rewrite prodvA prodv_id. suffices defVF: V_F = vspaceOver V. by exists V; split=> [||u]; rewrite ?defVF ?mem_vspaceOver ?idV. apply/vspaceP=> v; rewrite mem_vspaceOver idV. do [apply/idP/idP; last rewrite /V unlock] => [/coord_vbasis|/coord_span] ->. by apply: memv_suml => i _; rewrite memv_mul ?subvsP ?memv_span ?memt_nth. apply: memv_suml => i _; rewrite -tnth_nth; set xu := tnth _ i. have /allpairsP[[x u] /=]: xu \in _ := mem_tnth i _. case=> /vbasis_mem Fx /vbasis_mem Vu ->. rewrite scalerAl (coord_span Vu) mulr_sumr memv_suml // => j_. by rewrite -scalerCA (memvZ (Subvs _)) ?memvZ // vbasis_mem ?memt_nth. 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)