proposition: Lemma euclid b a c : coprimer a b -> (a %| c * b) = (a %| c) :> bool.
proof: Proof. move=> cab; symmetry. rewrite -{1}[c]mulr1 -(eqd_dvd (eqdd _) (eqd_mul (eqdd c) cab)). by rewrite (eqd_dvd (eqdd _) (mulr_gcdr _ _ _)) dvdr_gcd dvdr_mull. 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