proposition: Lemma det_diag_mx_seq_truncated m (s : seq R) : \det (diag_mx_seq m m s) = (\prod_(i <- take m s) i) *+ (m <= size s).
proof: Proof. elim: s m=> [[|m]|a l IHl [|m]]; rewrite ?det_mx00 ?leq0n ?take0 ?big_nil //. by rewrite diag_mx_seq_nil det0. rewrite big_cons ltnS diag_mx_seq_cons (@det_ublock _ 1 m). by rewrite IHl det_scalar expr1 mulrnAr. 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