proposition: Lemma mul_mxrow_mxcol m n (R_ : forall j, 'M[R]_(m, p_ j)) (C_ : forall i, 'M[R]_(p_ i, n)) : \mxrow_j R_ j *m \mxcol_i C_ i = \sum_i (R_ i *m C_ i).
proof: Proof. apply/matrixP => i j; rewrite !mxE summxE; under [RHS]eq_bigr do rewrite !mxE. rewrite sig_big_dep/= (reindex _ tagnat.sig_bij_on)/=. 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)