proposition: Lemma seq1_basis v : v != 0 -> basis_of <[v]> [:: v].
proof: Proof. by move=> nz_v; rewrite /basis_of span_seq1 // eqxx seq1_free. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)