proposition: Lemma diag0 m n : diag (0 : 'M[R]_(m,n)) = [::].
proof: Proof. rewrite /diag /smith_seq; case: smithP=> /= P d Q. rewrite mulmx0 mul0mx => /esym h0 _ _ _. have H : all (eq_op^~ 0) (take (minn m n) d). apply: (@diag_mx_seq_eq0 _ m n); first by rewrite size_take; case: leqP. by rewrite diag_mx_seq_take_min. by elim: (take (minn m n) d) H => //= a l h /andP [->] /=. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent