proposition: Lemma coord_span n (X : n.-tuple vT) v : v \in span X -> v = \sum_i coord X i v *: X`_i.
proof: Proof. rewrite memvK span_b2mx genmxE => Xv. by rewrite unlock_with mul_b2mx mulmxKpV ?v2rK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)