i j k : ℤ
⊢ Nat.lcm (Nat.lcm (natAbs i) (natAbs j)) (natAbs k) = Nat.lcm (natAbs i) (Nat.lcm (natAbs j) (natAbs k))
i j k : ℤ
⊢ lcm (↑(lcm i j)) k = lcm i ↑(lcm j k)
rw [Int.lcm, Int.lcm, Int.lcm, Int.lcm, natAbs_ofNat, natAbs_ofNat]
no goals
i j k : ℤ
⊢ Nat.lcm (Nat.lcm (natAbs i) (natAbs j)) (natAbs k) = Nat.lcm (natAbs i) (Nat.lcm (natAbs j) (natAbs k))
apply Nat.lcm_assoc