proposition: Lemma mem_baseVspace V : baseVspace V =i V.
proof: Proof. move=> y; apply/idP/idP=> [/coord_span->|/coord_vbasis->]; last first. apply: memv_suml => i _; rewrite (coordF (coord _ i (y : L))) scaler_suml -/n. apply: memv_suml => j _; rewrite -/bF -F0ZEZ memvZ ?memv_span // -!tnth_nth. by apply/imageP; exists (i, j). apply: memv_suml => k _; rewrite nth_image; case: (enum_val k) => i j /=. by rewrite F0ZEZ memvZ ?vbasis_mem ?mem_tnth. 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)