proposition: Lemma lcm_mul_mono_r : forall n m p, lcm (n * p) (m * p) == lcm n m * abs p.
proof: Proof. intros n m p. now rewrite !(mul_comm _ p), lcm_mul_mono_l, mul_comm. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor