proposition: Lemma mul_mxblock {R : ringType} {p q r : nat} {p_ : 'I_p -> nat} {q_ : 'I_q -> nat} {r_ : 'I_r -> nat} (A_ : forall i j, 'M[R]_(p_ i, q_ j)) (B_ : forall j k, 'M_(q_ j, r_ k)) : \mxblock_(i, j) A_ i j *m \mxblock_(j, k) B_ j k = \mxblock_(i, k) \sum_j (A_ i j *m B_ j k).
proof: Proof. rewrite mxblockEh mul_mxrow_mxblock mxblockEh; apply: eq_mxrow => i. by under [LHS]eq_bigr do rewrite mxcol_mul; rewrite -mxcol_sum. 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)