proposition: Lemma lcmrC a b : lcmr a b %= lcmr b a.
proof: Proof. case/boolP: (gcdr b a == 0) => [|H0]. by rewrite gcdr_eq0; case/andP => /eqP-> _; rewrite lcmr0 lcm0r. rewrite -(@eqd_mul2r _ (gcdr b a)) //. by rewrite (eqd_trans (eqd_mul (eqdd _) (gcdrC b a))) // !mulr_lcm_gcd mulrC. 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