proposition: Lemma mxdirect_sumsE (S_ : I -> mxsum_expr n n) (xunwrap := unwrap) : reflect (and (forall i, P i -> mxdirect (unwrap (S_ i))) (mxdirect (\sum_(i | P i) (xunwrap (S_ i))))) (mxdirect (\sum_(i | P i) (unwrap (S_ i)))).
proof: Proof. apply: (iffP (mxdirect_sums_recP _)) => [dxS | [dxS_ dxS] i Pi]. by do [split; last apply/mxdirect_sumsP] => i; case/dxS. by split; [apply: dxS_ | apply: mxdirect_sumsP Pi]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)