Lemmas relating / in ℤ with the ordering.

theorem Int.eq_mul_div_of_mul_eq_mul_of_dvd_left {a : ℤ} {b : ℤ} {c : ℤ} {d : ℤ} (hb : b ≠ 0) (hbc : b ∣ c) (h : b * a = c * d) : a = c / b * d

theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs {a : ℤ} {b : ℤ} (w : a ∣ b) (h : Int.natAbs b < Int.natAbs a) : b = 0

If an integer with larger absolute value divides an integer, it is zero.

theorem Int.eq_zero_of_dvd_of_nonneg_of_lt {a : ℤ} {b : ℤ} (w₁ : 0 ≤ a) (w₂ : a < b) (h : b ∣ a) : a = 0

theorem Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs {a : ℤ} {b : ℤ} {c : ℤ} (h1 : a % b = c) (h2 : Int.natAbs (a - c) < Int.natAbs b) : a = c

If two integers are congruent to a sufficiently large modulus, they are equal.

theorem Int.ofNat_add_negSucc_of_ge {m : ℕ} {n : ℕ} (h : Nat.succ n ≤ m) : Int.ofNat m + Int.negSucc n = Int.ofNat (m - Nat.succ n)

theorem Int.natAbs_le_of_dvd_ne_zero {s : ℤ} {t : ℤ} (hst : s ∣ t) (ht : t ≠ 0) : Int.natAbs s ≤ Int.natAbs t