proposition: Lemma egcdrP a b : egcdr_spec a b (egcdr a b).
proof: Proof. rewrite /egcdr; case: bezoutP=> x y hg /=. move: (dvdr_gcdr a b) (dvdr_gcdl a b); rewrite !(eqd_dvd hg (eqdd _))=> ha hb. have [g_eq0 | g_neq0] := boolP (_ == 0). rewrite (eqP g_eq0) eqdr0 in hg. move: (hg); rewrite gcdr_eq0=> /andP[/eqP-> /eqP->]. constructor; do ?by rewrite mulr0. by rewrite mulr0 addr0 mulr1. by rewrite eqd_sym gcdr0. constructor. move: hb ha. rewrite /dvdr. case: odivrP=> //= a1 Ha _. case: odivrP=> //= b1 Hb _. - apply/(mulIf g_neq0). by rewrite mulrDl mul1r -!mulrA -Ha -Hb. - by rewrite eqd_sym. - by move: hb; rewrite /dvdr; case: odivrP. by move: ha; rewrite /dvdr; case: odivrP. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete