proposition: Lemma diag_mx_seq_block s : let l := nseq (size s) 0%N in let F := (fun n i => (@scalar_mx _ n.+1 s`_i)) in diag_mx_seq (size_sum l).+1 (size_sum l).+1 s = diag_block_mx l F.
proof: Proof. case: s=> /= [|a l]; first by rewrite diag_mx_seq_nil. have Ha: forall a, diag_mx_seq 1 1 [:: a] = a%:M. by move=> b; apply/matrixP=> i j; rewrite !mxE ord1. elim: l a=> //= b l IHl a. by rewrite -IHl -cat1s (@diag_mx_seq_cat 1 _ 1) // Ha. 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