proposition: Lemma mulr_lcm_gcd a b : lcmr a b * gcdr a b = a * b.
proof: Proof. rewrite /lcmr /=; move: (dvdr_gcd_mul a b). have [-> | a0] := eqVneq a 0; first by rewrite !mul0r. have [-> | b0] := eqVneq b 0; first by rewrite !(mulr0, mul0r). by rewrite /dvdr; case: odivrP => // x. 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