proposition: Lemma dvdr_mul2r c a b : c != 0 -> (a * c %| b * c) = (a %| b) :> bool.
proof: Proof. move=> c0; apply/idP/idP=> [|hab]; last exact: dvdr_mul. case/dvdrP=> x /eqP; rewrite mulrA (inj_eq (mulIf _)) // => /eqP ->. exact: 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