proposition: Lemma gcdrE : forall a b, gcdr a b %= gcdr b (a %% b).
proof: Proof. move=> a b; rewrite /eqd dvdr_gcd dvdr_gcdr /=. case: edivP=> q r /= G _. move/eqP: (G); rewrite addrC -subr_eq; move/eqP=> H. rewrite -{1}H dvdr_sub ?dvdr_gcdl //; last by rewrite dvdr_mull ?dvdr_gcdr. by rewrite dvdr_gcd dvdr_gcdl G dvdr_add ?dvdr_gcdr // dvdr_mull ?dvdr_gcdl. 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