proposition: Lemma mul_diag_mx_copid m n r s : minn (minn m n) (size s) <= r -> diag_mx_seq m n s *m @copid_mx R n r = 0.
proof: Proof. move=> le_s_r; apply/matrixP=> i j; rewrite !mxE big1 // => k _; rewrite !mxE. case: eqP => /= [eq_i_k|]; last by rewrite mul0r. have [le_s_k|lt_k_s] := leqP (size s) k. by rewrite eq_i_k nth_default // mul0rn mul0r. suff ->/= : k < r by rewrite andbT eqE /= subrr mulr0. by apply: (leq_trans _ le_s_r); rewrite !leq_min lt_k_s -{1}eq_i_k !ltn_ord. 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