Results about the order properties of the integers, and the integers as an ordered ring.

Order properties of the integers

theorem Int.nonneg_def {a : Int} : a.NonNeg ↔ ∃ (n : Nat), a = ↑n

theorem Int.NonNeg.elim {a : Int} : a.NonNeg → ∃ (n : Nat), a = ↑n

theorem Int.nonneg_or_nonneg_neg (a : Int) : a.NonNeg ∨ (-a).NonNeg

theorem Int.le_def {a b : Int} : a ≤ b ↔ (b - a).NonNeg

theorem Int.lt_iff_add_one_le {a b : Int} : a < b ↔ a + 1 ≤ b

theorem Int.le.intro_sub {a b : Int} (n : Nat) (h : b - a = ↑n) : a ≤ b

theorem Int.le.intro {a b : Int} (n : Nat) (h : a + ↑n = b) : a ≤ b

theorem Int.le.dest_sub {a b : Int} (h : a ≤ b) : ∃ (n : Nat), b - a = ↑n

theorem Int.le.dest {a b : Int} (h : a ≤ b) : ∃ (n : Nat), a + ↑n = b

theorem Int.le_total (a b : Int) : a ≤ b ∨ b ≤ a

@[simp]

theorem Int.ofNat_le {m n : Nat} : ↑m ≤ ↑n ↔ m ≤ n

@[simp]

theorem Int.ofNat_zero_le (n : Nat) : 0 ≤ ↑n

theorem Int.eq_ofNat_of_zero_le {a : Int} (h : 0 ≤ a) : ∃ (n : Nat), a = ↑n

theorem Int.eq_succ_of_zero_lt {a : Int} (h : 0 < a) : ∃ (n : Nat), a = ↑n + 1

theorem Int.lt_add_succ (a : Int) (n : Nat) : a < a + (↑n + 1)

theorem Int.lt.intro {a b : Int} {n : Nat} (h : a + (↑n + 1) = b) : a < b

theorem Int.lt.dest {a b : Int} (h : a < b) : ∃ (n : Nat), a + ↑n.succ = b

@[simp]

theorem Int.ofNat_lt {n m : Nat} : ↑n < ↑m ↔ n < m

@[simp]

theorem Int.natCast_pos {n : Nat} : 0 < ↑n ↔ 0 < n

@[simp, deprecated Int.natCast_pos (since := "2025-05-13")]

theorem Int.ofNat_pos {n : Nat} : 0 < ↑n ↔ 0 < n

theorem Int.natCast_nonneg (n : Nat) : 0 ≤ ↑n

@[deprecated Int.natCast_nonneg (since := "2025-05-13")]

theorem Int.ofNat_nonneg (n : Nat) : 0 ≤ ↑n

theorem Int.ofNat_succ_pos (n : Nat) : 0 < ↑n.succ

@[simp]

theorem Int.le_refl (a : Int) : a ≤ a

theorem Int.le_rfl {a : Int} : a ≤ a

theorem Int.le_of_eq {a b : Int} (hab : a = b) : a ≤ b

theorem Int.ge_of_eq {a b : Int} (hab : a = b) : b ≤ a

theorem Int.le_trans {a b c : Int} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c

theorem Int.le_antisymm {a b : Int} (h₁ : a ≤ b) (h₂ : b ≤ a) : a = b

theorem Int.le_antisymm_iff {a b : Int} : a = b ↔ a ≤ b ∧ b ≤ a

@[simp]

theorem Int.lt_irrefl (a : Int) : ¬a < a

theorem Int.ne_of_lt {a b : Int} (h : a < b) : a ≠ b

theorem Int.ne_of_gt {a b : Int} (h : b < a) : a ≠ b

theorem Int.le_of_lt {a b : Int} (h : a < b) : a ≤ b

theorem Int.lt_iff_le_and_ne {a b : Int} : a < b ↔ a ≤ b ∧ a ≠ b

theorem Int.lt_succ (a : Int) : a < a + 1

theorem Int.zero_lt_one : 0 < 1

theorem Int.one_pos : 0 < 1

theorem Int.one_ne_zero : 1 ≠ 0

theorem Int.one_nonneg : 0 ≤ 1

theorem Int.lt_iff_le_not_le {a b : Int} : a < b ↔ a ≤ b ∧ ¬b ≤ a

theorem Int.lt_of_not_ge {a b : Int} (h : ¬a ≤ b) : b < a

theorem Int.not_le_of_gt {a b : Int} (h : b < a) : ¬a ≤ b

@[simp]

theorem Int.not_le {a b : Int} : ¬a ≤ b ↔ b < a

@[simp]

theorem Int.not_lt {a b : Int} : ¬a < b ↔ b ≤ a

theorem Int.lt_asymm {a b : Int} : a < b → ¬b < a

theorem Int.lt_or_le (a b : Int) : a < b ∨ b ≤ a

theorem Int.le_of_not_gt {a b : Int} (h : ¬a > b) : a ≤ b

theorem Int.not_lt_of_ge {a b : Int} (h : b ≤ a) : ¬a < b

theorem Int.lt_trichotomy (a b : Int) : a < b ∨ a = b ∨ b < a

theorem Int.ne_iff_lt_or_gt {a b : Int} : a ≠ b ↔ a < b ∨ b < a

theorem Int.lt_or_gt_of_ne {a b : Int} : a ≠ b → a < b ∨ b < a

theorem Int.lt_or_lt_of_ne {a b : Int} : a ≠ b → a < b ∨ b < a

theorem Int.eq_iff_le_and_ge {x y : Int} : x = y ↔ x ≤ y ∧ y ≤ x

theorem Int.le_iff_eq_or_lt {a b : Int} : a ≤ b ↔ a = b ∨ a < b

theorem Int.le_iff_lt_or_eq {a b : Int} : a ≤ b ↔ a < b ∨ a = b

theorem Int.lt_of_le_of_lt {a b c : Int} (h₁ : a ≤ b) (h₂ : b < c) : a < c

theorem Int.lt_of_lt_of_le {a b c : Int} (h₁ : a < b) (h₂ : b ≤ c) : a < c

theorem Int.lt_trans {a b c : Int} (h₁ : a < b) (h₂ : b < c) : a < c

instance Int.instTransLe : Trans (fun (x1 x2 : Int) => x1 ≤ x2) (fun (x1 x2 : Int) => x1 ≤ x2) fun (x1 x2 : Int) => x1 ≤ x2

instance Int.instTransLtLe : Trans (fun (x1 x2 : Int) => x1 < x2) (fun (x1 x2 : Int) => x1 ≤ x2) fun (x1 x2 : Int) => x1 < x2

instance Int.instTransLeLt : Trans (fun (x1 x2 : Int) => x1 ≤ x2) (fun (x1 x2 : Int) => x1 < x2) fun (x1 x2 : Int) => x1 < x2

instance Int.instTransLt : Trans (fun (x1 x2 : Int) => x1 < x2) (fun (x1 x2 : Int) => x1 < x2) fun (x1 x2 : Int) => x1 < x2

theorem Int.eq_natAbs_of_nonneg {a : Int} (h : 0 ≤ a) : a = ↑a.natAbs

@[reducible, inline, deprecated Int.eq_natAbs_of_nonneg (since := "2025-03-11")]

abbrev Int.eq_natAbs_of_zero_le {a : Int} (h : 0 ≤ a) : a = ↑a.natAbs

theorem Int.le_natAbs {a : Int} : a ≤ ↑a.natAbs

@[simp]

theorem Int.negSucc_lt_zero (n : Nat) : negSucc n < 0

theorem Int.negSucc_le_zero (n : Nat) : negSucc n ≤ 0

@[simp]

theorem Int.negSucc_not_nonneg (n : Nat) : 0 ≤ negSucc n ↔ False

theorem Int.add_le_add_left {a b : Int} (h : a ≤ b) (c : Int) : c + a ≤ c + b

theorem Int.add_lt_add_left {a b : Int} (h : a < b) (c : Int) : c + a < c + b

theorem Int.add_le_add_right {a b : Int} (h : a ≤ b) (c : Int) : a + c ≤ b + c

theorem Int.add_lt_add_right {a b : Int} (h : a < b) (c : Int) : a + c < b + c

theorem Int.le_of_add_le_add_left {a b c : Int} (h : a + b ≤ a + c) : b ≤ c

theorem Int.le_of_add_le_add_right {a b c : Int} (h : a + b ≤ c + b) : a ≤ c

@[simp]

theorem Int.add_le_add_iff_left {b c : Int} (a : Int) : a + b ≤ a + c ↔ b ≤ c

@[simp]

theorem Int.add_le_add_iff_right {a b : Int} (c : Int) : a + c ≤ b + c ↔ a ≤ b

theorem Int.add_le_add {a b c d : Int} (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d

theorem Int.le_add_of_nonneg_right {a b : Int} (h : 0 ≤ b) : a ≤ a + b

theorem Int.le_add_of_nonneg_left {a b : Int} (h : 0 ≤ b) : a ≤ b + a

theorem Int.neg_le_neg {a b : Int} (h : a ≤ b) : -b ≤ -a

@[simp]

theorem Int.neg_le_neg_iff {a b : Int} : -a ≤ -b ↔ b ≤ a

@[simp]

theorem Int.neg_le_zero_iff {a : Int} : -a ≤ 0 ↔ 0 ≤ a

@[simp]

theorem Int.zero_le_neg_iff {a : Int} : 0 ≤ -a ↔ a ≤ 0

theorem Int.le_of_neg_le_neg {a b : Int} (h : -b ≤ -a) : a ≤ b

theorem Int.neg_nonpos_of_nonneg {a : Int} (h : 0 ≤ a) : -a ≤ 0

theorem Int.neg_nonneg_of_nonpos {a : Int} (h : a ≤ 0) : 0 ≤ -a

theorem Int.neg_lt_neg {a b : Int} (h : a < b) : -b < -a

@[simp]

theorem Int.neg_lt_neg_iff {a b : Int} : -a < -b ↔ b < a

@[simp]

theorem Int.neg_lt_zero_iff {a : Int} : -a < 0 ↔ 0 < a

@[simp]

theorem Int.zero_lt_neg_iff {a : Int} : 0 < -a ↔ a < 0

theorem Int.neg_neg_of_pos {a : Int} (h : 0 < a) : -a < 0

theorem Int.neg_pos_of_neg {a : Int} (h : a < 0) : 0 < -a

theorem Int.sub_nonneg_of_le {a b : Int} (h : b ≤ a) : 0 ≤ a - b

theorem Int.le_of_sub_nonneg {a b : Int} (h : 0 ≤ a - b) : b ≤ a

theorem Int.sub_pos_of_lt {a b : Int} (h : b < a) : 0 < a - b

theorem Int.lt_of_sub_pos {a b : Int} (h : 0 < a - b) : b < a

theorem Int.sub_left_le_of_le_add {a b c : Int} (h : a ≤ b + c) : a - b ≤ c

theorem Int.sub_le_self (a : Int) {b : Int} (h : 0 ≤ b) : a - b ≤ a

theorem Int.sub_lt_self (a : Int) {b : Int} (h : 0 < b) : a - b < a

theorem Int.add_one_le_of_lt {a b : Int} (H : a < b) : a + 1 ≤ b

theorem Int.le_iff_lt_add_one {a b : Int} : a ≤ b ↔ a < b + 1

theorem Int.min_def (n m : Int) : min n m = if n ≤ m then n else m

theorem Int.max_def (n m : Int) : max n m = if n ≤ m then m else n

@[simp]

theorem Int.neg_min_neg (a b : Int) : min (-a) (-b) = -max a b

@[simp]

theorem Int.min_add_right (a b c : Int) : min (a + c) (b + c) = min a b + c

@[simp]

theorem Int.min_add_left (a b c : Int) : min (a + b) (a + c) = a + min b c

theorem Int.min_comm (a b : Int) : min a b = min b a

instance Int.instCommutativeMin : Std.Commutative min

theorem Int.min_le_right (a b : Int) : min a b ≤ b

theorem Int.min_le_left (a b : Int) : min a b ≤ a

theorem Int.min_eq_left {a b : Int} (h : a ≤ b) : min a b = a

theorem Int.min_eq_right {a b : Int} (h : b ≤ a) : min a b = b

theorem Int.le_min {a b c : Int} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c

theorem Int.lt_min {a b c : Int} : a < min b c ↔ a < b ∧ a < c

@[simp]

theorem Int.neg_max_neg (a b : Int) : max (-a) (-b) = -min a b

@[simp]

theorem Int.max_add_right (a b c : Int) : max (a + c) (b + c) = max a b + c

@[simp]

theorem Int.max_add_left (a b c : Int) : max (a + b) (a + c) = a + max b c

theorem Int.max_comm (a b : Int) : max a b = max b a

instance Int.instCommutativeMax : Std.Commutative max

theorem Int.le_max_left (a b : Int) : a ≤ max a b

theorem Int.le_max_right (a b : Int) : b ≤ max a b

theorem Int.max_eq_right {a b : Int} (h : a ≤ b) : max a b = b

theorem Int.max_eq_left {a b : Int} (h : b ≤ a) : max a b = a

theorem Int.max_le {a b c : Int} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c

theorem Int.max_lt {a b c : Int} : max a b < c ↔ a < c ∧ b < c

@[simp]

theorem Int.ofNat_max_zero (n : Nat) : max (↑n) 0 = ↑n

@[simp]

theorem Int.zero_max_ofNat (n : Nat) : max 0 ↑n = ↑n

@[simp]

theorem Int.negSucc_max_zero (n : Nat) : max (negSucc n) 0 = 0

@[simp]

theorem Int.zero_max_negSucc (n : Nat) : max 0 (negSucc n) = 0

@[simp]

theorem Int.min_self (a : Int) : min a a = a

instance Int.instIdempotentOpMin : Std.IdempotentOp min

@[simp]

theorem Int.max_self (a : Int) : max a a = a

instance Int.instIdempotentOpMax : Std.IdempotentOp max

theorem Int.mul_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a * b

theorem Int.mul_pos {a b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a * b

theorem Int.mul_lt_mul_of_pos_left {a b c : Int} (h₁ : a < b) (h₂ : 0 < c) : c * a < c * b

theorem Int.mul_lt_mul_of_pos_right {a b c : Int} (h₁ : a < b) (h₂ : 0 < c) : a * c < b * c

theorem Int.mul_le_mul_of_nonneg_left {a b c : Int} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : c * a ≤ c * b

theorem Int.mul_le_mul_of_nonneg_right {a b c : Int} (h₁ : a ≤ b) (h₂ : 0 ≤ c) : a * c ≤ b * c

theorem Int.mul_le_mul {a b c d : Int} (hac : a ≤ c) (hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) : a * b ≤ c * d

theorem Int.mul_nonpos_of_nonneg_of_nonpos {a b : Int} (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0

theorem Int.mul_nonpos_of_nonpos_of_nonneg {a b : Int} (ha : a ≤ 0) (hb : 0 ≤ b) : a * b ≤ 0

theorem Int.mul_le_mul_of_nonpos_right {a b c : Int} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

theorem Int.mul_le_mul_of_nonpos_left {a b c : Int} (ha : a ≤ 0) (h : c ≤ b) : a * b ≤ a * c

@[simp]

theorem Int.natAbs_natCast (n : Nat) : (↑n).natAbs = n

@[deprecated Int.natAbs_natCast (since := "2025-04-16")]

theorem Int.natAbs_ofNat (n : Nat) : (↑n).natAbs = n

@[simp]

theorem Int.natAbs_ofNat' (n : Nat) : (ofNat n).natAbs = n

@[simp]

theorem Int.natAbs_negSucc (n : Nat) : (negSucc n).natAbs = n.succ

@[simp]

theorem Int.natAbs_zero : natAbs 0 = 0

@[simp]

theorem Int.natAbs_one : natAbs 1 = 1

@[simp]

theorem Int.natAbs_eq_zero {a : Int} : a.natAbs = 0 ↔ a = 0

@[simp]

theorem Int.natAbs_pos {a : Int} : 0 < a.natAbs ↔ a ≠ 0

@[simp]

theorem Int.natAbs_neg (a : Int) : (-a).natAbs = a.natAbs

theorem Int.natAbs_eq (a : Int) : a = ↑a.natAbs ∨ a = -↑a.natAbs

theorem Int.natAbs_negOfNat (n : Nat) : (negOfNat n).natAbs = n

theorem Int.natAbs_mul (a b : Int) : (a * b).natAbs = a.natAbs * b.natAbs

theorem Int.natAbs_eq_natAbs_iff {a b : Int} : a.natAbs = b.natAbs ↔ a = b ∨ a = -b

theorem Int.natAbs_of_nonneg {a : Int} (H : 0 ≤ a) : ↑a.natAbs = a

theorem Int.ofNat_natAbs_of_nonpos {a : Int} (H : a ≤ 0) : ↑a.natAbs = -a

theorem Int.eq_neg_natAbs_of_nonpos {a : Int} (h : a ≤ 0) : a = -↑a.natAbs

theorem Int.natAbs_sub_of_nonneg_of_le {a b : Int} (h₁ : 0 ≤ b) (h₂ : b ≤ a) : (a - b).natAbs = a.natAbs - b.natAbs

theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs {d n : Int} (h : d ∣ n) (h₁ : n.natAbs < d.natAbs) : n = 0

toNat

theorem Int.toNat_eq_max (a : Int) : ↑a.toNat = max a 0

@[simp]

theorem Int.toNat_zero : toNat 0 = 0

@[simp]

theorem Int.toNat_one : toNat 1 = 1

theorem Int.toNat_of_nonneg {a : Int} (h : 0 ≤ a) : ↑a.toNat = a

@[simp]

theorem Int.toNat_natCast (n : Nat) : (↑n).toNat = n

@[deprecated Int.toNat_natCast (since := "2025-04-16")]

theorem Int.toNat_ofNat (n : Nat) : (↑n).toNat = n

@[simp]

theorem Int.toNat_negSucc (n : Nat) : (negSucc n).toNat = 0

@[simp]

theorem Int.toNat_natCast_add_one {n : Nat} : (↑n + 1).toNat = n + 1

@[deprecated Int.toNat_natCast_add_one (since := "2025-04-16")]

theorem Int.toNat_ofNat_add_one {n : Nat} : (↑n + 1).toNat = n + 1

@[simp]

theorem Int.ofNat_toNat (a : Int) : ↑a.toNat = max a 0

theorem Int.self_le_toNat (a : Int) : a ≤ ↑a.toNat

@[simp]

theorem Int.le_toNat {n : Nat} {z : Int} (h : 0 ≤ z) : n ≤ z.toNat ↔ ↑n ≤ z

@[simp]

theorem Int.toNat_lt {n : Nat} {z : Int} (h : 0 ≤ z) : z.toNat < n ↔ z < ↑n

theorem Int.toNat_add {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a + b).toNat = a.toNat + b.toNat

theorem Int.toNat_mul {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a * b).toNat = a.toNat * b.toNat

theorem Int.toNat_sub'' {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : (a - b).toNat = a.toNat - b.toNat

Variant of Int.toNat_sub taking non-negativity hypotheses, rather than expecting the arguments to be casts of natural numbers.

theorem Int.toNat_add_nat {a : Int} (ha : 0 ≤ a) (n : Nat) : (a + ↑n).toNat = a.toNat + n

@[simp]

theorem Int.pred_toNat (i : Int) : (i - 1).toNat = i.toNat - 1

theorem Int.toNat_sub_toNat_neg (n : Int) : ↑n.toNat - ↑(-n).toNat = n

@[simp]

theorem Int.toNat_add_toNat_neg_eq_natAbs (n : Int) : n.toNat + (-n).toNat = n.natAbs

@[simp]

theorem Int.toNat_neg_nat (n : Nat) : (-↑n).toNat = 0

toNat?

theorem Int.mem_toNat? {a : Int} {n : Nat} : a.toNat? = some n ↔ a = ↑n

@[reducible, inline, deprecated Int.mem_toNat? (since := "2025-03-11")]

abbrev Int.mem_toNat' {a : Int} {n : Nat} : a.toNat? = some n ↔ a = ↑n

Order properties of the integers

theorem Int.le_of_not_le {a b : Int} : ¬a ≤ b → b ≤ a

@[simp]

theorem Int.negSucc_not_pos (n : Nat) : 0 < negSucc n ↔ False

theorem Int.eq_negSucc_of_lt_zero {a : Int} : a < 0 → ∃ (n : Nat), a = negSucc n

theorem Int.lt_of_add_lt_add_left {a b c : Int} (h : a + b < a + c) : b < c

theorem Int.lt_of_add_lt_add_right {a b c : Int} (h : a + b < c + b) : a < c

@[simp]

theorem Int.add_lt_add_iff_left {b c : Int} (a : Int) : a + b < a + c ↔ b < c

@[simp]

theorem Int.add_lt_add_iff_right {a b : Int} (c : Int) : a + c < b + c ↔ a < b

theorem Int.add_lt_add {a b c d : Int} (h₁ : a < b) (h₂ : c < d) : a + c < b + d

theorem Int.add_lt_add_of_le_of_lt {a b c d : Int} (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d

theorem Int.add_lt_add_of_lt_of_le {a b c d : Int} (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d

theorem Int.lt_add_of_pos_right (a : Int) {b : Int} (h : 0 < b) : a < a + b

theorem Int.lt_add_of_pos_left (a : Int) {b : Int} (h : 0 < b) : a < b + a

theorem Int.add_nonneg {a b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b

theorem Int.add_pos {a b : Int} (ha : 0 < a) (hb : 0 < b) : 0 < a + b

theorem Int.add_pos_of_pos_of_nonneg {a b : Int} (ha : 0 < a) (hb : 0 ≤ b) : 0 < a + b

theorem Int.add_pos_of_nonneg_of_pos {a b : Int} (ha : 0 ≤ a) (hb : 0 < b) : 0 < a + b

theorem Int.add_nonpos {a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) : a + b ≤ 0

theorem Int.add_neg {a b : Int} (ha : a < 0) (hb : b < 0) : a + b < 0

theorem Int.add_neg_of_neg_of_nonpos {a b : Int} (ha : a < 0) (hb : b ≤ 0) : a + b < 0

theorem Int.add_neg_of_nonpos_of_neg {a b : Int} (ha : a ≤ 0) (hb : b < 0) : a + b < 0

theorem Int.lt_add_of_le_of_pos {a b c : Int} (hbc : b ≤ c) (ha : 0 < a) : b < c + a

theorem Int.add_one_le_iff {a b : Int} : a + 1 ≤ b ↔ a < b

theorem Int.lt_add_one_iff {a b : Int} : a < b + 1 ↔ a ≤ b

@[simp]

theorem Int.succ_ofNat_pos (n : Nat) : 0 < ↑n + 1

theorem Int.not_ofNat_neg (n : Nat) : ¬↑n < 0

theorem Int.le_add_one {a b : Int} (h : a ≤ b) : a ≤ b + 1

theorem Int.nonneg_of_neg_nonpos {a : Int} (h : -a ≤ 0) : 0 ≤ a

theorem Int.nonpos_of_neg_nonneg {a : Int} (h : 0 ≤ -a) : a ≤ 0

theorem Int.lt_of_neg_lt_neg {a b : Int} (h : -b < -a) : a < b

theorem Int.pos_of_neg_neg {a : Int} (h : -a < 0) : 0 < a

theorem Int.neg_of_neg_pos {a : Int} (h : 0 < -a) : a < 0

theorem Int.le_neg_of_le_neg {a b : Int} (h : a ≤ -b) : b ≤ -a

theorem Int.neg_le_of_neg_le {a b : Int} (h : -a ≤ b) : -b ≤ a

theorem Int.lt_neg_of_lt_neg {a b : Int} (h : a < -b) : b < -a

theorem Int.neg_lt_of_neg_lt {a b : Int} (h : -a < b) : -b < a

@[simp]

theorem Int.neg_pos {a : Int} : 0 < -a ↔ a < 0

@[simp]

theorem Int.neg_nonneg {a : Int} : 0 ≤ -a ↔ a ≤ 0

@[simp]

theorem Int.neg_neg_iff_pos {a : Int} : -a < 0 ↔ 0 < a

theorem Int.sub_nonpos_of_le {a b : Int} (h : a ≤ b) : a - b ≤ 0

theorem Int.le_of_sub_nonpos {a b : Int} (h : a - b ≤ 0) : a ≤ b

theorem Int.sub_neg_of_lt {a b : Int} (h : a < b) : a - b < 0

@[simp]

theorem Int.sub_pos {a b : Int} : 0 < a - b ↔ b < a

@[simp]

theorem Int.sub_nonneg {a b : Int} : 0 ≤ a - b ↔ b ≤ a

theorem Int.lt_of_sub_neg {a b : Int} (h : a - b < 0) : a < b

theorem Int.add_le_of_le_neg_add {a b c : Int} (h : b ≤ -a + c) : a + b ≤ c

theorem Int.le_neg_add_of_add_le {a b c : Int} (h : a + b ≤ c) : b ≤ -a + c

theorem Int.add_le_of_le_sub_left {a b c : Int} (h : b ≤ c - a) : a + b ≤ c

theorem Int.le_sub_left_of_add_le {a b c : Int} (h : a + b ≤ c) : b ≤ c - a

theorem Int.add_le_of_le_sub_right {a b c : Int} (h : a ≤ c - b) : a + b ≤ c

theorem Int.le_sub_right_of_add_le {a b c : Int} (h : a + b ≤ c) : a ≤ c - b

theorem Int.le_add_of_neg_add_le {a b c : Int} (h : -b + a ≤ c) : a ≤ b + c

theorem Int.neg_add_le_of_le_add {a b c : Int} (h : a ≤ b + c) : -b + a ≤ c

theorem Int.le_add_of_sub_left_le {a b c : Int} (h : a - b ≤ c) : a ≤ b + c

theorem Int.le_add_of_sub_right_le {a b c : Int} (h : a - c ≤ b) : a ≤ b + c

theorem Int.sub_right_le_of_le_add {a b c : Int} (h : a ≤ b + c) : a - c ≤ b

theorem Int.le_add_of_neg_add_le_left {a b c : Int} (h : -b + a ≤ c) : a ≤ b + c

theorem Int.neg_add_le_left_of_le_add {a b c : Int} (h : a ≤ b + c) : -b + a ≤ c

theorem Int.le_add_of_neg_add_le_right {a b c : Int} (h : -c + a ≤ b) : a ≤ b + c

theorem Int.neg_add_le_right_of_le_add {a b c : Int} (h : a ≤ b + c) : -c + a ≤ b

theorem Int.le_add_of_neg_le_sub_left {a b c : Int} (h : -a ≤ b - c) : c ≤ a + b

theorem Int.neg_le_sub_left_of_le_add {a b c : Int} (h : c ≤ a + b) : -a ≤ b - c

theorem Int.le_add_of_neg_le_sub_right {a b c : Int} (h : -b ≤ a - c) : c ≤ a + b

theorem Int.neg_le_sub_right_of_le_add {a b c : Int} (h : c ≤ a + b) : -b ≤ a - c

theorem Int.sub_le_of_sub_le {a b c : Int} (h : a - b ≤ c) : a - c ≤ b

theorem Int.sub_le_sub_left {a b : Int} (h : a ≤ b) (c : Int) : c - b ≤ c - a

theorem Int.sub_le_sub_right {a b : Int} (h : a ≤ b) (c : Int) : a - c ≤ b - c

theorem Int.sub_le_sub {a b c d : Int} (hab : a ≤ b) (hcd : c ≤ d) : a - d ≤ b - c

theorem Int.le_of_sub_le_sub_left {a b c : Int} (h : c - a ≤ c - b) : b ≤ a

theorem Int.le_of_sub_le_sub_right {a b c : Int} (h : a - c ≤ b - c) : a ≤ b

@[simp]

theorem Int.sub_le_sub_left_iff {a b c : Int} : c - a ≤ c - b ↔ b ≤ a

@[simp]

theorem Int.sub_le_sub_right_iff {a b c : Int} : a - c ≤ b - c ↔ a ≤ b

theorem Int.add_lt_of_lt_neg_add {a b c : Int} (h : b < -a + c) : a + b < c

theorem Int.lt_neg_add_of_add_lt {a b c : Int} (h : a + b < c) : b < -a + c

theorem Int.add_lt_of_lt_sub_left {a b c : Int} (h : b < c - a) : a + b < c

theorem Int.lt_sub_left_of_add_lt {a b c : Int} (h : a + b < c) : b < c - a

theorem Int.add_lt_of_lt_sub_right {a b c : Int} (h : a < c - b) : a + b < c

theorem Int.lt_sub_right_of_add_lt {a b c : Int} (h : a + b < c) : a < c - b

theorem Int.lt_add_of_neg_add_lt {a b c : Int} (h : -b + a < c) : a < b + c

theorem Int.neg_add_lt_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c

theorem Int.lt_add_of_sub_left_lt {a b c : Int} (h : a - b < c) : a < b + c

theorem Int.sub_left_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - b < c

theorem Int.lt_add_of_sub_right_lt {a b c : Int} (h : a - c < b) : a < b + c

theorem Int.sub_right_lt_of_lt_add {a b c : Int} (h : a < b + c) : a - c < b

theorem Int.lt_add_of_neg_add_lt_left {a b c : Int} (h : -b + a < c) : a < b + c

theorem Int.neg_add_lt_left_of_lt_add {a b c : Int} (h : a < b + c) : -b + a < c

theorem Int.lt_add_of_neg_add_lt_right {a b c : Int} (h : -c + a < b) : a < b + c

theorem Int.neg_add_lt_right_of_lt_add {a b c : Int} (h : a < b + c) : -c + a < b

theorem Int.lt_add_of_neg_lt_sub_left {a b c : Int} (h : -a < b - c) : c < a + b

theorem Int.neg_lt_sub_left_of_lt_add {a b c : Int} (h : c < a + b) : -a < b - c

theorem Int.lt_add_of_neg_lt_sub_right {a b c : Int} (h : -b < a - c) : c < a + b

theorem Int.neg_lt_sub_right_of_lt_add {a b c : Int} (h : c < a + b) : -b < a - c

theorem Int.add_lt_iff {a b c : Int} : a + b < c ↔ a < -b + c

theorem Int.sub_lt_iff {a b c : Int} : a - b < c ↔ a < c + b

theorem Int.sub_lt_of_sub_lt {a b c : Int} (h : a - b < c) : a - c < b

theorem Int.sub_lt_sub_left {a b : Int} (h : a < b) (c : Int) : c - b < c - a

theorem Int.sub_lt_sub_right {a b : Int} (h : a < b) (c : Int) : a - c < b - c

theorem Int.sub_lt_sub {a b c d : Int} (hab : a < b) (hcd : c < d) : a - d < b - c

theorem Int.lt_of_sub_lt_sub_left {a b c : Int} (h : c - a < c - b) : b < a

theorem Int.lt_of_sub_lt_sub_right {a b c : Int} (h : a - c < b - c) : a < b

@[simp]

theorem Int.sub_lt_sub_left_iff {a b c : Int} : c - a < c - b ↔ b < a

@[simp]

theorem Int.sub_lt_sub_right_iff {a b c : Int} : a - c < b - c ↔ a < b

theorem Int.sub_lt_sub_of_le_of_lt {a b c d : Int} (hab : a ≤ b) (hcd : c < d) : a - d < b - c

theorem Int.sub_lt_sub_of_lt_of_le {a b c d : Int} (hab : a < b) (hcd : c ≤ d) : a - d < b - c

theorem Int.add_le_add_three {a b c d e f : Int} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a + b + c ≤ d + e + f

theorem Int.exists_eq_neg_ofNat {a : Int} (H : a ≤ 0) : ∃ (n : Nat), a = -↑n

theorem Int.lt_of_add_one_le {a b : Int} (H : a + 1 ≤ b) : a < b

theorem Int.lt_add_one_of_le {a b : Int} (H : a ≤ b) : a < b + 1

theorem Int.le_of_lt_add_one {a b : Int} (H : a < b + 1) : a ≤ b

theorem Int.sub_one_lt_of_le {a b : Int} (H : a ≤ b) : a - 1 < b

theorem Int.le_of_sub_one_lt {a b : Int} (H : a - 1 < b) : a ≤ b

theorem Int.le_sub_one_of_lt {a b : Int} (H : a < b) : a ≤ b - 1

theorem Int.lt_of_le_sub_one {a b : Int} (H : a ≤ b - 1) : a < b

theorem Int.le_add_one_iff {m n : Int} : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

theorem Int.sub_one_lt_iff {m n : Int} : m - 1 < n ↔ m ≤ n

theorem Int.le_sub_one_iff {m n : Int} : m ≤ n - 1 ↔ m < n

theorem Int.add_le_iff_le_sub {a b c : Int} : a + b ≤ c ↔ a ≤ c - b

theorem Int.le_add_iff_sub_le {a b c : Int} : a ≤ b + c ↔ a - c ≤ b

theorem Int.add_le_zero_iff_le_neg {a b : Int} : a + b ≤ 0 ↔ a ≤ -b

theorem Int.add_le_zero_iff_le_neg' {a b : Int} : a + b ≤ 0 ↔ b ≤ -a

theorem Int.add_nonnneg_iff_neg_le {a b : Int} : 0 ≤ a + b ↔ -b ≤ a

theorem Int.add_nonnneg_iff_neg_le' {a b : Int} : 0 ≤ a + b ↔ -a ≤ b

theorem Int.mul_lt_mul {a b c d : Int} (h₁ : a < c) (h₂ : b ≤ d) (h₃ : 0 < b) (h₄ : 0 ≤ c) : a * b < c * d

theorem Int.mul_lt_mul' {a b c d : Int} (h₁ : a ≤ c) (h₂ : b < d) (h₃ : 0 ≤ b) (h₄ : 0 < c) : a * b < c * d

theorem Int.mul_neg_of_pos_of_neg {a b : Int} (ha : 0 < a) (hb : b < 0) : a * b < 0

theorem Int.mul_neg_of_neg_of_pos {a b : Int} (ha : a < 0) (hb : 0 < b) : a * b < 0

theorem Int.mul_nonneg_of_nonpos_of_nonpos {a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) : 0 ≤ a * b

theorem Int.mul_lt_mul_of_neg_left {a b c : Int} (h : b < a) (hc : c < 0) : c * a < c * b

theorem Int.mul_lt_mul_of_neg_right {a b c : Int} (h : b < a) (hc : c < 0) : a * c < b * c

theorem Int.mul_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a * b

theorem Int.mul_self_le_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a ≤ b) : a * a ≤ b * b

theorem Int.mul_self_lt_mul_self {a b : Int} (h1 : 0 ≤ a) (h2 : a < b) : a * a < b * b

theorem Int.nonneg_of_mul_nonneg_left {a b : Int} (h : 0 ≤ a * b) (hb : 0 < b) : 0 ≤ a

theorem Int.nonneg_of_mul_nonneg_right {a b : Int} (h : 0 ≤ a * b) (ha : 0 < a) : 0 ≤ b

theorem Int.nonpos_of_mul_nonpos_left {a b : Int} (h : a * b ≤ 0) (hb : 0 < b) : a ≤ 0

theorem Int.nonpos_of_mul_nonpos_right {a b : Int} (h : a * b ≤ 0) (ha : 0 < a) : b ≤ 0

theorem Int.nonneg_of_mul_nonpos_left {a b : Int} (h : a * b ≤ 0) (hb : b < 0) : 0 ≤ a

theorem Int.nonneg_of_mul_nonpos_right {a b : Int} (h : a * b ≤ 0) (ha : a < 0) : 0 ≤ b

theorem Int.nonpos_of_mul_nonneg_left {a b : Int} (h : 0 ≤ a * b) (hb : b < 0) : a ≤ 0

theorem Int.nonpos_of_mul_nonneg_right {a b : Int} (h : 0 ≤ a * b) (ha : a < 0) : b ≤ 0

theorem Int.pos_of_mul_pos_left {a b : Int} (h : 0 < a * b) (hb : 0 < b) : 0 < a

theorem Int.pos_of_mul_pos_right {a b : Int} (h : 0 < a * b) (ha : 0 < a) : 0 < b

theorem Int.neg_of_mul_neg_left {a b : Int} (h : a * b < 0) (hb : 0 < b) : a < 0

theorem Int.neg_of_mul_neg_right {a b : Int} (h : a * b < 0) (ha : 0 < a) : b < 0

theorem Int.pos_of_mul_neg_left {a b : Int} (h : a * b < 0) (hb : b < 0) : 0 < a

theorem Int.pos_of_mul_neg_right {a b : Int} (h : a * b < 0) (ha : a < 0) : 0 < b

theorem Int.neg_of_mul_pos_left {a b : Int} (h : 0 < a * b) (hb : b < 0) : a < 0

theorem Int.neg_of_mul_pos_right {a b : Int} (h : 0 < a * b) (ha : a < 0) : b < 0

@[simp]

theorem Int.sign_zero : sign 0 = 0

@[simp]

theorem Int.sign_one : sign 1 = 1

theorem Int.sign_neg_one : (-1).sign = -1

@[simp]

theorem Int.sign_of_add_one (x : Nat) : (↑x + 1).sign = 1

@[simp]

theorem Int.sign_negSucc (x : Nat) : (negSucc x).sign = -1

theorem Int.natAbs_sign (z : Int) : z.sign.natAbs = if z = 0 then 0 else 1

theorem Int.natAbs_sign_of_ne_zero {z : Int} (hz : z ≠ 0) : z.sign.natAbs = 1

@[deprecated Int.natAbs_sign_of_ne_zero (since := "2025-04-16")]

theorem Int.natAbs_sign_of_nonzero {z : Int} (hz : z ≠ 0) : z.sign.natAbs = 1

theorem Int.sign_natCast_of_ne_zero {n : Nat} (hn : n ≠ 0) : (↑n).sign = 1

@[deprecated Int.sign_natCast_of_ne_zero (since := "2025-04-16")]

theorem Int.sign_ofNat_of_nonzero {n : Nat} (hn : n ≠ 0) : (↑n).sign = 1

@[simp]

theorem Int.sign_neg (z : Int) : (-z).sign = -z.sign

theorem Int.sign_mul_natAbs (a : Int) : a.sign * ↑a.natAbs = a

@[simp]

theorem Int.sign_mul (a b : Int) : (a * b).sign = a.sign * b.sign

theorem Int.sign_eq_one_of_pos {a : Int} (h : 0 < a) : a.sign = 1

theorem Int.sign_eq_neg_one_of_neg {a : Int} (h : a < 0) : a.sign = -1

theorem Int.eq_zero_of_sign_eq_zero {a : Int} : a.sign = 0 → a = 0

theorem Int.pos_of_sign_eq_one {a : Int} : a.sign = 1 → 0 < a

theorem Int.neg_of_sign_eq_neg_one {a : Int} : a.sign = -1 → a < 0

@[simp]

theorem Int.sign_eq_one_iff_pos {a : Int} : a.sign = 1 ↔ 0 < a

@[simp]

theorem Int.sign_eq_neg_one_iff_neg {a : Int} : a.sign = -1 ↔ a < 0

@[simp]

theorem Int.sign_eq_zero_iff_zero {a : Int} : a.sign = 0 ↔ a = 0

@[simp]

theorem Int.sign_sign {x : Int} : x.sign.sign = x.sign

@[simp]

theorem Int.sign_nonneg_iff {x : Int} : 0 ≤ x.sign ↔ 0 ≤ x

@[reducible, inline, deprecated Int.sign_nonneg_iff (since := "2025-03-11")]

abbrev Int.sign_nonneg {x : Int} : 0 ≤ x.sign ↔ 0 ≤ x

@[simp]

theorem Int.sign_pos_iff {x : Int} : 0 < x.sign ↔ 0 < x

@[simp]

theorem Int.sign_nonpos_iff {x : Int} : x.sign ≤ 0 ↔ x ≤ 0

@[simp]

theorem Int.sign_neg_iff {x : Int} : x.sign < 0 ↔ x < 0

@[simp]

theorem Int.mul_sign_self (i : Int) : i * i.sign = ↑i.natAbs

@[reducible, inline, deprecated Int.mul_sign_self (since := "2025-02-24")]

abbrev Int.mul_sign (i : Int) : i * i.sign = ↑i.natAbs

@[simp]

theorem Int.sign_mul_self (i : Int) : i.sign * i = ↑i.natAbs

theorem Int.sign_trichotomy (a : Int) : a.sign = 1 ∨ a.sign = 0 ∨ a.sign = -1

theorem Int.natAbs_ne_zero {a : Int} : a.natAbs ≠ 0 ↔ a ≠ 0

theorem Int.natAbs_mul_self {a : Int} : ↑(a.natAbs * a.natAbs) = a * a

theorem Int.eq_nat_or_neg (a : Int) : ∃ (n : Nat), a = ↑n ∨ a = -↑n

theorem Int.natAbs_mul_natAbs_eq {a b : Int} {c : Nat} (h : a * b = ↑c) : a.natAbs * b.natAbs = c

@[simp]

theorem Int.natAbs_mul_self' (a : Int) : ↑a.natAbs * ↑a.natAbs = a * a

theorem Int.natAbs_eq_iff {a : Int} {n : Nat} : a.natAbs = n ↔ a = ↑n ∨ a = -↑n

theorem Int.natAbs_add_le (a b : Int) : (a + b).natAbs ≤ a.natAbs + b.natAbs

theorem Int.natAbs_sub_le (a b : Int) : (a - b).natAbs ≤ a.natAbs + b.natAbs

theorem Int.natAbs_add_of_nonneg {a b : Int} : 0 ≤ a → 0 ≤ b → (a + b).natAbs = a.natAbs + b.natAbs

theorem Int.natAbs_add_of_nonpos {a b : Int} (ha : a ≤ 0) (hb : b ≤ 0) : (a + b).natAbs = a.natAbs + b.natAbs

@[deprecated Int.negSucc_eq (since := "2025-03-11")]

theorem Int.negSucc_eq' (m : Nat) : negSucc m = -↑m - 1

theorem Int.natAbs_lt_natAbs_of_nonneg_of_lt {a b : Int} (w₁ : 0 ≤ a) (w₂ : a < b) : a.natAbs < b.natAbs

theorem Int.natAbs_eq_iff_mul_eq_zero {a : Int} {n : Nat} : a.natAbs = n ↔ (a - ↑n) * (a + ↑n) = 0

@[reducible, inline, deprecated Int.natAbs_eq_iff_mul_eq_zero (since := "2025-03-11")]

abbrev Int.eq_natAbs_iff_mul_eq_zero {a : Int} {n : Nat} : a.natAbs = n ↔ (a - ↑n) * (a + ↑n) = 0