proposition: Lemma egcdr3P a b c : egcdr3_spec a b c (egcdr3 a b c).
proof: Proof. rewrite /egcdr3; case: egcdrP=> /= g' u1 v1 b1 c1 heq hg' hb1 hc1. case: egcdrP=> /= g u v a1 g1 heq' hg ha1 hg1. constructor; rewrite -?mulrA -?hg1 ?(eqd_trans hg) ?eqd_gcd //. by rewrite -addrA -mulrDr !mulrA -mulrDl heq mul1r. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr