proposition: Lemma mul_mxdiag_mxcol m (D_ : forall i, 'M[R]_(p_ i)) (C_ : forall i, 'M[R]_(p_ i, m)): \mxdiag_i D_ i *m \mxcol_i C_ i = \mxcol_i (D_ i *m C_ i).
proof: Proof. rewrite /mxdiag mxblockEh mul_mxrow_mxcol. under [LHS]eq_bigr do rewrite mxcol_mul; rewrite -mxcol_sum. apply/eq_mxcol => i; rewrite (bigD1 i)//= eqxx conform_mx_id big1 ?addr0//. by move=> j; case: eqVneq => //=; rewrite mul0mx. 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)