proposition: Lemma diag_mx_seq_nil m n : diag_mx_seq m n [::] = 0.
proof: Proof. by apply/matrixP=> i j; rewrite !mxE nth_nil mul0rn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm poly mxpoly finfun tuple) mathcomp(matrix bigop zmodp polydiv) ssrcomplements dvdring