proposition: Lemma sorted_Smith n m (M: 'M[E]_(n,m)): sorted (@dvdr E) (Smith_seq M).
proof: Proof. rewrite /Smith_seq. case: (SmithP find1P find2P find_pivotP) => L0 d R0 _ H HL0 HR0. case: d H=> //= a l H. have/allP Ha: all (%|%R a) l by exact: (order_path_min (@dvdr_trans _)). rewrite path_min_sorted; [exact: (path_sorted H) | apply/allP=> x Hx]. apply/(dvdr_trans _ (Ha x Hx))/dvdrP; exists (\det R0 * \det L0). by rewrite -invrM ?mulVKr // unitrM -!unitmxE HR0. 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)