proposition: Lemma coord_basis U n (X : n.-tuple vT) v : basis_of U X -> v \in U -> v = \sum_i coord X i v *: X`_i.
proof: Proof. by move/span_basis <-; apply: coord_span. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)