proposition: Lemma span_def X : span X = (\sum_(u <- X) <[u]>)%VS.
proof: Proof. apply/subv_anti/andP; split. by apply/span_subvP=> v Xv; rewrite (big_rem v) // memvE addvSl. by rewrite big_tnth; apply/subv_sumP=> i _; rewrite -memvE memv_span ?mem_tnth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)