proposition: Lemma diag_mx_seq_cons m n x (s : seq R) : diag_mx_seq (1 + m) (1 + n) (x :: s) = block_mx x%:M 0 0 (diag_mx_seq m n s).
proof: Proof. apply/matrixP => i j; rewrite !mxE. by case: splitP => i' ->; rewrite mxE; case:splitP => j' ->; rewrite mxE ?ord1. 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