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