proposition: Lemma Smith_unicity m n (M : 'M[R]_(m,n)) (d : seq R) : sorted %|%R d -> equivalent M (diag_mx_seq m n d) -> forall i, i < minn m n -> d`_i %= (smith_seq M)`_i.
proof: Proof. rewrite /smith_seq=> Hd HMd i. case: smithP=> P s Q heq Hsorted Punitmx Qunitmx /=. have HMdmt : equivalent M (diag_mx_seq m n s). by split=> //; exists P; exists Q; split=> //; rewrite conform_mx_id. elim: i {-2}i (leqnn i)=>[i|i IHi j Hji Hj]. rewrite leqn0=> /eqP -> Hi. move: (Smith_gcdr_spec Hi Hd HMd); rewrite eqd_sym. move/(eqd_trans (Smith_gcdr_spec Hi Hsorted HMdmt)). by rewrite !big_ord1 eqd_sym. move: (Smith_gcdr_spec Hj Hd HMd); rewrite eqd_sym. move/(eqd_trans (Smith_gcdr_spec Hj Hsorted HMdmt)). rewrite !big_ord_recr /= => H3. have H1: \prod_(i < j) d`_i %= \prod_(i < j) s`_i. apply: eqd_big_mul=> k _. by rewrite (IHi k _ (ltn_trans _ Hj)) // -ltnS (leq_trans (ltn_ord k) Hji). have [H0|H0] := boolP (\prod_(i < j) d`_i == 0). have/prodf_eq0 [k _ /eqP Hk] : (\prod_(i < j) s`_i == 0). by rewrite (eqP H0) eqd0r in H1. case/prodf_eq0: H0 => l _ /eqP Hl. move: (sorted_nth0 (sorted_drop k Hsorted) (j - k)). move: (sorted_nth0 (sorted_drop l Hd) (j - l)). rewrite !nth_drop !addn0 Hk Hl !dvd0r (subnKC (ltnW (ltn_ord k))). by rewrite (subnKC (ltnW (ltn_ord l)))=> /eqP -> /eqP ->. by rewrite -(eqd_mul2l _ _ H0) (eqd_rtrans (eqd_mulr _ H1)) eqd_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path tuple) mathcomp(perm fingroup choice ssralg fintype finfun poly polydiv) mathcomp(bigop matrix zmodp mxalgebra) ssrcomplements dvdring mxstructure similar minor binetcauchy stronglydiscrete coherent