proposition: Lemma diag_mx_seq_take_min m n (s : seq R) : diag_mx_seq m n (take (minn m n) s) = diag_mx_seq m n s.
proof: Proof. by case: leqP; rewrite (diag_mx_seq_takel, diag_mx_seq_taker). 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