proposition: Lemma bezout_edrP a b : bezout_spec a b (bezout_edr a b).
proof: Proof. have := erefl (gcd_edr a b); rewrite {-1}/gcd_edr /smith_seq. rewrite /bezout_edr; case: smithP => /= P d Q heq hsorted Punitmx Qunitmx hg. constructor; rewrite /gcdr /= hg. 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 -{1}(lshift0 1 0) mxE (row_mxEl a%:M) 2!mxE (row_mxEr a%:M) !mxE !mulr1n. by rewrite mulrAC [_ * b * _]mulrAC=> ->. 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