proposition: Lemma euclid_gcdr a b c : coprimer a b -> gcdr a (c * b) %= gcdr a c.
proof: Proof. move=> cab. rewrite eqd_def !dvdr_gcd !dvdr_gcdl /= andbC dvdr_mulr //= -(@euclid b) //. rewrite /coprimer (eqd_trans (gcdrAC _ _ _)) //. by rewrite (eqd_trans (eqd_gcd cab (eqdd _))) ?gcd1r. 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