proposition: Lemma mul_copid_mx_diag m n r s : minn (minn m n) (size s) <= r -> @copid_mx R n r *m diag_mx_seq n m s = 0.
proof: Proof. move=> le_s_r. rewrite -[_ *m _]trmxK trmx_mul tr_diag_mx_seq tr_copid_mx. by rewrite mul_diag_mx_copid // trmx0. 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