proposition: Lemma eqd_gcd c d a b : a %= c -> b %= d -> gcdr a b %= gcdr c d.
proof: Proof. move=> ac bd; rewrite eqd_def !dvdr_gcd -(eqd_dvd (eqdd _) ac) dvdr_gcdl. rewrite -(eqd_dvd (eqdd _) bd) dvdr_gcdr (eqd_dvd (eqdd _) ac) dvdr_gcdl. by rewrite (eqd_dvd (eqdd _) bd) dvdr_gcdr. 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