proposition: Lemma memv_sumr P vs (Us : I -> {vspace vT}) : (forall i, P i -> vs i \in Us i) -> \sum_(i | P i) vs i \in (\sum_(i | P i) Us i)%VS.
proof: Proof. by move=> Uv; apply/rpred_sum=> i Pi; apply/(sumv_sup i Pi)/Uv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)