proposition: Lemma diag_mx_seq_block_mx m m' n n' s : size s <= minn m n -> diag_mx_seq (m + m') (n + n') s = block_mx (diag_mx_seq m n s) 0 0 0.
proof: Proof. move=> H; apply/matrixP=> i j; rewrite !mxE. case: (splitP _)=> k Hk; rewrite mxE; case: (splitP _)=> l Hl; rewrite mxE Hk Hl //. + case: eqP => //= ->. rewrite nth_default ?mul0rn // (leq_trans H) //. by rewrite geq_min leq_addr orbT. + rewrite nth_default ?mul0rn // (leq_trans H) //. by rewrite geq_min leq_addr. rewrite nth_default ?mul0rn // (leq_trans H) //. by rewrite geq_min leq_addr. 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