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