proposition: Lemma lcm_abs_l : forall n m, lcm (abs n) m == lcm n m.
proof: Proof. intros n m. destruct (abs_eq_or_opp n) as [H|H]; rewrite H. - easy. - apply lcm_opp_l. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor