proposition: Lemma coord_sum_free n (X : n.-tuple vT) k j : free X -> coord X j (\sum_(i < n) k i *: X`_i) = k j.
proof: Proof. move=> Xfree; rewrite linear_sum (bigD1 j) ?linearZ //= coord_free // eqxx. rewrite mulr1 big1 ?addr0 // => i /negPf j'i. by rewrite linearZ /= coord_free // j'i mulr0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)