proposition: Lemma lcm_opp_l : forall n m, lcm (-n) m == lcm n m.
proof: Proof. intros. apply lcm_unique_alt; try apply lcm_nonneg. intros. rewrite divide_opp_l. apply lcm_divide_iff. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor