proposition: Lemma sorted_invf n (A : 'M[F]_n) : sorted (@dvdp _) (invariant_factors A).
proof: Proof. have := sorted_Frobenius_seq A. rewrite Frobenius_seqE. apply: subseq_sorted. exact: dvdp_trans. exact: suffix_subseq. 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)