proposition: Lemma lcmr_mull a b : lcmr a (a * b) %= a * b.
proof: Proof. have [-> | a0] := eqVneq a 0; first by rewrite mul0r /eqd !lcm0r dvdr0. rewrite -{1}[a]mulr1 (eqd_trans (lcmr_mul2l 1 b a)) // eqd_mul2l //. exact: (lcm1r b). 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