proposition: Lemma nnil_inv_factors n (A : 'M_n.+1) : invariant_factors A != [::].
proof: Proof. apply: contraPneq (sum_size_inv_factors A) => ->. by rewrite big_nil. 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 companion closed_poly smith_complements)