proposition: Lemma free_span X v (sumX := fun k => \sum_(x <- X) k x *: x) : free X -> v \in <<X>>%VS -> {k | v = sumX k & forall k1, v = sumX k1 -> {in X, k1 =1 k}}.
proof: Proof. rewrite -{2}[X]in_tupleE => freeX /coord_span def_v. pose k x := oapp (fun i => coord (in_tuple X) i v) 0 (insub (index x X)). exists k => [|k1 {}def_v _ /(nthP 0)[i ltiX <-]]. rewrite /sumX (big_nth 0) big_mkord def_v; apply: eq_bigr => i _. by rewrite /k index_uniq ?free_uniq // valK. rewrite /k /= index_uniq ?free_uniq // insubT //= def_v. by rewrite /sumX (big_nth 0) big_mkord coord_sum_free. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)