proposition: Fact subvs_vect_iso : Vector.axiom (\dim U) subvs_of.
proof: Proof. exists (fun w => \row_i coord (vbasis U) i (vsval w)). by move=> k w1 w2; apply/rowP=> i; rewrite !mxE linearP. exists (fun rw : 'rV_(\dim U) => vsproj (\sum_i rw 0 i *: (vbasis U)`_i)). move=> w /=; congr (vsproj _ = w): (vsvalK w). by rewrite {1}(coord_vbasis (subvsP w)); apply: eq_bigr => i _; rewrite mxE. move=> rw; apply/rowP=> i; rewrite mxE vsprojK. by rewrite coord_sum_free ?(basis_free (vbasisP U)). by apply: rpred_sum => j _; rewrite rpredZ ?vbasis_mem ?memt_nth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)