proposition: Lemma gcdr_mul2r a b c : gcdr (a * c) (b * c) %= gcdr a b * c.
proof: Proof. rewrite /eqd !dvdr_gcd !dvdr_mul // !andbT. case c0: (c == 0); first by rewrite (eqP c0) !mulr0 dvdr0. have Hc: c %| gcdr (a * c) (b * c) by rewrite dvdr_gcd !dvdr_mull //. case/dvdrP: Hc=> g Hg. rewrite Hg dvdr_mul // dvdr_gcd -![g %| _](@dvdr_mul2r _ c) ?c0 //. by rewrite -Hg dvdr_gcdl 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