proposition: Lemma equiv_Smith n m (M: 'M[E]_(n,m)) : equivalent M (Smith_form M).
proof: Proof. case: n m M=>[m M|n]; first exact: equiv0l. case=>[M|m M]; first exact: equiv0r. rewrite /Smith_form /Smith_seq. case: (SmithP find1P find2P find_pivotP) => L0 d R0 H _ HL0 HR0; split=> //. exists ((@block_mx _ 1 _ 1 _ ((\det L0)^-1 / \det R0)%:M 0 0 1%:M) *m L0). exists R0; split=> //. rewrite unitmxE detM unitrM (@det_lblock _ 1 n) det_scalar1 det1 mulr1. by rewrite unitrM !unitrV -!unitmxE HL0 HR0. rewrite conform_mx_id -!mulmxA (mulmxA L0) H. case: d H =>[|a l _] ; first by rewrite !diag_mx_seq_nil mulmx0. rewrite !diag_mx_seq_cons (@mulmx_block _ 1 _ 1 _ 1). by rewrite !mulmx0 !mul0mx !add0r addr0 mul1mx -scalar_mxM. 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)