proposition: Lemma sub_span X Y : {subset X <= Y} -> (<<X>> <= <<Y>>)%VS.
proof: Proof. by move=> sXY; apply/span_subvP=> v /sXY/memv_span. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)