proposition: Lemma mxdirect_sumsP (A_ : I -> 'M_n) : reflect (forall i, P i -> A_ i :&: (\sum_(j | P j && (j != i)) A_ j) = 0)%MS (mxdirect (\sum_(i | P i) A_ i)).
proof: Proof. apply: (iffP (mxdirect_sums_recP _)) => dxA i /dxA; first by case. by rewrite mxdirect_trivial. 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)