proposition: Lemma vbasis1 : exists2 k, k != 0 & vbasis 1 = [:: k%:A] :> seq aT.
proof: Proof. move: (vbasis 1) (@vbasisP K aT 1); rewrite dim_vline oner_neq0. case/tupleP=> x X0; rewrite {X0}tuple0 => defX; have Xx := mem_head x nil. have /vlineP[k def_x] := basis_mem defX Xx; exists k; last by rewrite def_x. by have:= basis_not0 defX Xx; rewrite def_x scaler_eq0 oner_eq0 orbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop ssralg) mathcomp(finalg zmodp matrix vector poly)