proposition: Lemma Smith_gcdr_spec : \prod_(i < k) s`_i %= \big[(@gcdr [the gcdDomainType of R : Type])/0]_(f : {ffun 'I_k -> 'I_m}) (\big[(@gcdr [the gcdDomainType of R : Type])/0]_(g : {ffun 'I_k -> 'I_n}) minor f g A).
proof: Proof. rewrite (eqd_ltrans eqd_seq_gcdr). have [ _ _ [M [N [_ _ Heqs]]]] := HAs. have [ _ _ [P [Q [_ _ Hseq]]]] := equiv_sym HAs. rewrite conform_mx_id in Heqs. rewrite conform_mx_id in Hseq. have HdivmA p q k1 (B C : 'M[R]_(p,q)) (M1 : 'M_p) (N1 : 'M_q) : forall (H : M1 *m C *m N1 = B), forall (f : 'I_k1 -> 'I_p) (g : 'I_k1 -> 'I_q), \big[(@gcdr [the gcdDomainType of R : Type])/0]_(f0 : {ffun 'I_k1 -> 'I_p}) \big[(@gcdr [the gcdDomainType of R : Type])/0]_(g0 : {ffun 'I_k1 -> 'I_q}) minor f0 g0 C %| minor f g B. move=> H f g. have HBC: minor f g B = \sum_(f0 : {ffun 'I__ -> 'I__ } | strictf f0) ((\sum_(g0 : {ffun 'I__ -> 'I__ } | strictf g0) (minor id g0 (submatrix f id M1) * minor g0 f0 C)) * minor f0 id (submatrix id g N1)). rewrite -H /minor submatrix_mul BinetCauchy. apply: eq_bigr=> i _; congr GRing.mul; rewrite /minor. rewrite sub_submatrix submatrix_mul BinetCauchy. by apply: eq_bigr=> j _; rewrite /minor !sub_submatrix. rewrite HBC; apply: big_dvdr=> h; rewrite dvdr_mulr //. apply: big_dvdr=> j; rewrite dvdr_mull //. by apply: (dvdr_trans (big_dvdr_gcdr _ j)); apply: big_dvdr_gcdr. apply/andP; split; apply: big_gcdrP=> f; apply: big_gcdrP=> g. exact: (HdivmA _ _ _ _ _ _ _ Hseq). exact: (HdivmA _ _ _ _ _ _ _ Heqs). 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