proposition: Lemma diag_mxC n (d e : 'rV[R]_n) : diag_mx d *m diag_mx e = diag_mx e *m diag_mx d.
proof: Proof. by rewrite !mulmx_diag; congr (diag_mx _); apply/rowP=> i; rewrite !mxE mulrC. 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)