proposition: Lemma lcm_assoc : forall n m p, lcm n (lcm m p) == lcm (lcm n m) p.
proof: Proof. intros. apply lcm_unique_alt; try apply lcm_nonneg. intros. now rewrite !lcm_divide_iff, and_assoc. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs ZGcd ZDivTrunc ZDivFloor