proposition: Lemma mulr_lcmr a b c : a * lcmr b c %= lcmr (a * b) (a * c).
proof: Proof. case/boolP: ((a * b == 0) && (a * c == 0)) => [/andP[] | H0]. rewrite mulf_eq0; case/orP => /eqP->. by rewrite !mul0r lcm0r. by rewrite mulr0 !lcm0r mulr0. rewrite -(@eqd_mul2r _ (gcdr (a * b) (a * c))) ?gcdr_eq0 // mulr_lcm_gcd. rewrite eqd_sym (eqd_trans _ (eqd_mul (eqdd _) (mulr_gcdr a b c))) //. by rewrite -!mulrA [lcmr b c * _]mulrCA mulr_lcm_gcd [b * _]mulrCA. 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