proposition: Lemma size_Smith_seq n (M: 'M[E]_n) : \det M != 0 -> size (take n (Smith_seq M)) = n.
proof: Proof. move=> HdM0; rewrite size_take; apply: minn_idPl. apply: contra_neqT HdM0=>/negbTE H. by rewrite -det_Smith /Smith_form det_diag_mx_seq_truncated H. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image)