proposition: Lemma euclid_inv a b c : coprimer a b -> (a * b %| c) = (a %| c) && (b %| c).
proof: Proof. move=> cab. by rewrite -mulr_lcm_gcd (eqd_dvd (eqd_mul (eqdd _) cab) (eqdd _)) mulr1 dvdr_lcm. 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