proposition: Lemma memv_span X v : v \in X -> v \in <<X>>%VS.
proof: Proof. by case/seq_tnthP=> i {v}->; rewrite unlock memvK genmxE (eq_row_sub i) // rowK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)