i j : ℤ
⊢ j ∣ ↑(Nat.lcm (natAbs i) (natAbs j))
i j : ℤ
⊢ j ∣ ↑(lcm i j)
rw [Int.lcm]
i j : ℤ
⊢ natAbs j ∣ Nat.lcm (natAbs i) (natAbs j)
i j : ℤ
⊢ j ∣ ↑(Nat.lcm (natAbs i) (natAbs j))
apply coe_nat_dvd_right.mpr
no goals
i j : ℤ
⊢ natAbs j ∣ Nat.lcm (natAbs i) (natAbs j)
apply Nat.dvd_lcm_right