proposition: Lemma gcd_edrP d a b : (d %| gcd_edr a b)%R = (d %| a)%R && (d %| b)%R.
proof: Proof. rewrite /gcd_edr /smith_seq; case: smithP => /= P ds Q heq _ Punitmx Qunitmx. apply/idP/andP => [gd0|[gdvda gdvdb]]. suff Hij : forall i j, d %| (row_mx a%:M b%:M : 'rV_2) i j. move: (Hij 0 (@lshift 1 1 0)) (Hij 0 (rshift 1 0)). by rewrite (row_mxEl a%:M) (row_mxEr a%:M) !mxE !mulr1n. move/(canRL (mulmxK Qunitmx))/(canRL (mulKmx Punitmx)): heq ->. apply/dvdr_mulmxl/dvdr_mulmxr=> i j. by rewrite ord1 {i} mxE; case: j => [[]] //= _ _; rewrite mulr0n dvdr0. move/matrixP: heq => /(_ 0 0). rewrite [P]mx11_scalar mul_scalar_mx !mxE big_ord_recl big_ord1 -rshift1 mulr1n. have -> : ord0 = 0 by []. rewrite -(lshift0 1 0) mxE (row_mxEl a%:M) 2!mxE (row_mxEr a%:M) => <-. by rewrite -!mulrA -mulrDr dvdr_mull // dvdr_add ?dvdr_mulr ?mxE. 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