proposition: Lemma dvdr_lcm a b c : (lcmr a b %| c) = (a %| c) && (b %| c) :> bool.
proof: Proof. have [-> | a0] := eqVneq a 0. rewrite lcm0r dvd0r. by case: eqP => //= ->; rewrite dvdr0. have [-> | b0] := eqVneq b 0. rewrite lcmr0 dvd0r andbC. by case: eqP => //= ->; rewrite dvdr0. rewrite -(@dvdr_mul2r _ (gcdr a b)); last by rewrite gcdr_eq0 negb_and a0. rewrite mulr_lcm_gcd (eqd_dvd (eqdd _) (mulr_gcdr _ _ _)) dvdr_gcd {1}mulrC. by rewrite !dvdr_mul2r // andbC. 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