proposition: Lemma diag_mx_seq_cat m1 m2 n1 n2 (s1 s2 : seq R) : size s1 = m1 -> size s1 = n1 -> diag_mx_seq (m1 + m2) (n1 + n2) (s1 ++ s2) = block_mx (diag_mx_seq m1 n1 s1) 0 0 (diag_mx_seq m2 n2 s2).
proof: Proof. elim: s1 s2 m1 n1=> [s2 m1 n1 Hn1 Hn2|a s1 IHs1 s2 m1 n1 /eqP Hm1 /eqP Hn1]. by rewrite /block_mx -Hn1 -Hn2 !row_thin_mx col_flat_mx. case:m1 Hm1 IHs1=> // m1 Hm1 IHs1; case:n1 Hn1 IHs1=> // n1 Hn1 IHs1. rewrite diag_mx_seq_cons IHs1; apply/eqP=> //; rewrite diag_mx_seq_cons. by rewrite -row_mx0 -col_mx0 block_mxA castmx_id row_mx0 col_mx0. 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