proposition: Lemma submxblock_sum (I : finType) (B_ : forall k, 'M[V]_(sp, sq)) (P : {pred I}) i j : submxblock (\sum_(k | P k) B_ k) i j = \sum_(k | P k) submxblock (B_ k) i j.
proof: Proof. apply/matrixP => k l; rewrite !(mxE, summxE). by apply: eq_bigr => p; rewrite !mxE. 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 countalg finalg zmodp)