Lemmas relating `/` in `ℤ` with the ordering. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_nat_abs_lt_nat_abs {a b : ℤ} (w : a ∣ b) (h : b.nat_abs < a.nat_abs) :

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_nat_abs_sub_lt_nat_abs {a b c : ℤ} (h1 : a % b = c) (h2 : (a - c).nat_abs < b.nat_abs) :

a = c

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

theorem int.of_nat_add_neg_succ_of_nat_of_ge {m n : ℕ} (h : n.succ ≤ m) :

theorem int.nat_abs_le_of_dvd_ne_zero {s t : ℤ} (hst : s ∣ t) (ht : t ≠ 0) :

Lemmas relating / in ℤ with the ordering. #