proposition: Lemma vbasisP U : basis_of U (vbasis U).
proof: Proof. rewrite /basis_of free_b2mx span_b2mx (sameP eqP (vs2mxP _ _)) !genmxE. have ->: b2mx (vbasis U) = row_base (vs2mx U). by apply/row_matrixP=> i; rewrite unlock rowK tnth_mktuple r2vK. by rewrite row_base_free !eq_row_base submx_refl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)