proposition: Lemma directv_sumE {Ss : I -> addv_expr} (xunwrap := unwrap) : reflect [/\ forall i, P i -> directv (unwrap (Ss i)) & directv (\sum_(i | P i) xunwrap (Ss i))] (directv (\sum_(i | P i) unwrap (Ss i))).
proof: Proof. by rewrite !directvE /= /dimv 2!{1}vs2mx_sum -!mxdirectE; apply: mxdirect_sumsE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)