proposition: Lemma mul_diag_mx m n d (A : 'M_(m, n)) : diag_mx d *m A = \matrix_(i, j) (d 0 i * A i j).
proof: Proof. apply/matrixP=> i j; rewrite !mxE (bigD1 i) //= mxE eqxx big1 ?addr0 // => i'. by rewrite mxE eq_sym mulrnAl => /negPf->. 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)