proposition: Lemma Smith_unicity n (A : 'M[E]_n) (s : seq E) : sorted %|%R s -> equivalent A (diag_mx_seq n n s) -> forall i, (i < n)%N -> s`_i %= (Smith_seq A)`_i.
proof: Proof. move=> Hs HAs i. have Hsmt := sorted_Smith A. have HAsmt := equiv_Smith A. elim: i {-2}i (leqnn i)=>[i|i IHi j Hji]. rewrite leqn0 -[X in (i < X)%N]minnn=> /eqP -> Hi. move: (Smith_gcdr_spec Hi Hs HAs). move: (Smith_gcdr_spec Hi Hsmt HAsmt). rewrite !big_ord_recl !big_ord0 !mulr1 eqd_sym => H1 H2. exact: (eqd_trans H2 H1). rewrite -[X in (j < X)%N]minnn=> Hj. move: (Smith_gcdr_spec Hj Hs HAs). move: (Smith_gcdr_spec Hj Hsmt HAsmt). rewrite !big_ord_recr /= eqd_sym => H1 H2. have {H1 H2} H3:= eqd_trans H2 H1. have H1: \prod_(i < j) s`_i %= \prod_(i < j) (Smith_seq A)`_i. rewrite minnn in Hj. apply: eqd_big_mul=> k _; apply: IHi. exact: (leq_trans (ltn_ord k) Hji). exact: (ltn_trans _ Hj). case: (eqVneq (\prod_(i < j) s`_i) 0) => H0; last first. by rewrite -(eqd_mul2l _ _ H0) (eqd_rtrans (eqd_mulr _ H1)). have/prodf_eq0 [k _ /eqP Hk]: (\prod_(i < j) (Smith_seq A)`_i == 0). by rewrite H0 eqd0r in H1. case/eqP/prodf_eq0: H0 => l _ /eqP Hl. have sj0 : s`_j == 0. have [ jlts | slej ] := ltnP j (size s); last first. by rewrite (nth_default 0 slej). rewrite -dvd0r -{1}Hl. apply: sorted_leq_nth => //. + exact: dvdr_trans. + by rewrite inE (ltn_trans _ jlts). + exact: ltnW. have smsj0 : (Smith_seq A)`_j == 0. have [ jlts | slej ] := ltnP j (size (Smith_seq A)); last first. by rewrite (nth_default 0 slej). rewrite -dvd0r -{1}Hk. apply: sorted_leq_nth => //. + exact: dvdr_trans. + by rewrite inE (ltn_trans _ jlts). + exact: ltnW. by rewrite (eqP sj0) (eqP smsj0). 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)