# Further lemmas about `Int` relying on `omega` automation. #

### miscellaneous lemmas #

source
@[simp]
theorem Int.natCast_le_zero {n : Nat} :
↑n ≤ 0 ↔ n = 0
source
@[simp]
theorem Int.neg_nonpos_iff (i : Int) :
-i ≤ 0 ↔ 0 ≤ i
source
@[simp]
theorem Int.zero_le_ofNat (n : Nat) :
0 ≤ OfNat.ofNat n
source
@[simp]
theorem Int.neg_natCast_le_natCast (n m : Nat) :
-↑n ≤ ↑m
source
@[simp]
theorem Int.neg_natCast_le_ofNat (n m : Nat) :
-↑n ≤ OfNat.ofNat m
source
@[simp]
theorem Int.neg_ofNat_le_ofNat (n m : Nat) :
-OfNat.ofNat n ≤ OfNat.ofNat m
source
@[simp]
theorem Int.neg_ofNat_le_natCast (n m : Nat) :
-OfNat.ofNat n ≤ ↑m
source
theorem Int.neg_lt_self_iff {n : Int} :
-n < n ↔ 0 < n
source
theorem Int.ofNat_add_out (m n : Nat) :
↑m + ↑n = ↑(m + n)
source
theorem Int.ofNat_mul_out (m n : Nat) :
↑m * ↑n = ↑(m * n)
source
theorem Int.ofNat_add_one_out (n : Nat) :
↑n + 1 = ↑n.succ
source
@[simp]
theorem Int.ofNat_eq_natCast (n : Nat) :
ofNat n = ↑n
source
theorem Int.natCast_inj {m n : Nat} :
↑m = ↑n ↔ m = n
source
theorem Int.natCast_sub {n m : Nat} :
n ≤ m → ↑(m - n) = ↑m - ↑n
source
theorem Int.natCast_ne_zero {n : Nat} :
↑n ≠ 0 ↔ n ≠ 0
source
theorem Int.natCast_ne_zero_iff_pos {n : Nat} :
↑n ≠ 0 ↔ 0 < n
source
theorem Int.natCast_succ_pos (n : Nat) :
0 < ↑n.succ
source
@[simp]
theorem Int.natCast_nonpos_iff {n : Nat} :
↑n ≤ 0 ↔ n = 0
source
@[simp]
theorem Int.sign_natCast_add_one (n : Nat) :
(↑n + 1).sign = 1
source
@[simp]
theorem Int.cast_id {n : Int} :
↑n = n
source
@[simp]
theorem Int.ble'_eq_true (a b : Int) :
(a.ble' b = true) = (a ≤ b)
source
@[simp]
theorem Int.blt'_eq_true (a b : Int) :
(a.blt' b = true) = (a < b)
source
@[simp]
theorem Int.ble'_eq_false (a b : Int) :
(a.ble' b = false) = ¬a ≤ b
source
@[simp]
theorem Int.blt'_eq_false (a b : Int) :
(a.blt' b = false) = ¬a < b

### toNat #

source
@[simp]
theorem Int.toNat_sub' (a : Int) (b : Nat) :
(a - ↑b).toNat = a.toNat - b
source
@[simp]
theorem Int.toNat_sub_max_self (a : Int) :
(a - max a 0).toNat = 0
source
@[simp]
theorem Int.toNat_sub_self_max (a : Int) :
(a - max 0 a).toNat = 0
source
@[simp]
theorem Int.toNat_eq_zero {n : Int} :
n.toNat = 0 ↔ n ≤ 0
source
@[simp]
theorem Int.toNat_le {m : Int} {n : Nat} :
m.toNat ≤ n ↔ m ≤ ↑n
source
@[simp]
theorem Int.toNat_lt' {m : Int} {n : Nat} (hn : 0 < n) :
m.toNat < n ↔ m < ↑n
source
@[simp]
theorem Int.lt_toNat {m : Nat} {n : Int} :
m < n.toNat ↔ ↑m < n
source
theorem Int.lt_of_toNat_lt {a b : Int} (h : a.toNat < b.toNat) :
a < b
source
theorem Int.toNat_sub_of_le {a b : Int} (h : b ≤ a) :
↑(a - b).toNat = a - b
source
theorem Int.pos_iff_toNat_pos {n : Int} :
0 < n ↔ 0 < n.toNat
source
theorem Int.natCast_toNat_eq_self {a : Int} :
↑a.toNat = a ↔ 0 ≤ a
source
@[deprecated Int.natCast_toNat_eq_self (since := "2025-04-16")]
theorem Int.ofNat_toNat_eq_self {a : Int} :
↑a.toNat = a ↔ 0 ≤ a
source
theorem Int.eq_natCast_toNat {a : Int} :
a = ↑a.toNat ↔ 0 ≤ a
source
@[deprecated Int.eq_natCast_toNat (since := "2025-04-16")]
theorem Int.eq_ofNat_toNat {a : Int} :
a = ↑a.toNat ↔ 0 ≤ a
source
theorem Int.toNat_le_toNat {n m : Int} (h : n ≤ m) :
n.toNat ≤ m.toNat
source
theorem Int.toNat_lt_toNat {n m : Int} (hn : 0 < m) :
n.toNat < m.toNat ↔ n < m

### min and max #

source
@[simp]
theorem Int.min_assoc (a b c : Int) :
min (min a b) c = min a (min b c)
source
instance Int.instAssociativeMin :
Std.Associative min
source
@[simp]
theorem Int.min_self_assoc {m n : Int} :
min m (min m n) = min m n
source
@[simp]
theorem Int.min_self_assoc' {m n : Int} :
min n (min m n) = min n m
source
@[simp]
theorem Int.max_assoc (a b c : Int) :
max (max a b) c = max a (max b c)
source
instance Int.instAssociativeMax :
Std.Associative max
source
@[simp]
theorem Int.max_self_assoc {m n : Int} :
max m (max m n) = max m n
source
@[simp]
theorem Int.max_self_assoc' {m n : Int} :
max n (max m n) = max n m
source
theorem Int.max_min_distrib_left (a b c : Int) :
max a (min b c) = min (max a b) (max a c)
source
theorem Int.min_max_distrib_left (a b c : Int) :
min a (max b c) = max (min a b) (min a c)
source
theorem Int.max_min_distrib_right (a b c : Int) :
max (min a b) c = min (max a c) (max b c)
source
theorem Int.min_max_distrib_right (a b c : Int) :
min (max a b) c = max (min a c) (min b c)
source
theorem Int.sub_min_sub_right (a b c : Int) :
min (a - c) (b - c) = min a b - c
source
theorem Int.sub_max_sub_right (a b c : Int) :
max (a - c) (b - c) = max a b - c
source
theorem Int.sub_min_sub_left (a b c : Int) :
min (a - b) (a - c) = a - max b c
source
theorem Int.sub_max_sub_left (a b c : Int) :
max (a - b) (a - c) = a - min b c

## mul #

source
theorem Int.mul_le_mul_of_natAbs_le {x y : Int} {s t : Nat} (hx : x.natAbs ≤ s) (hy : y.natAbs ≤ t) :
x * y ≤ ↑s * ↑t
source
theorem Int.mul_le_mul_of_le_of_le_of_nonneg_of_nonpos {a b c d : Int} (hac : a ≤ c) (hbd : d ≤ b) (hb : 0 ≤ b) (hc : c ≤ 0) :
a * b ≤ c * d

This is a generalization of `a ≤ c` and `b ≤ d` implying `a * b ≤ c * d` for natural numbers, appropriately generalized to integers when `b` is nonnegative and `c` is nonpositive.

source
theorem Int.mul_le_mul_of_le_of_le_of_nonneg_of_nonneg {a b c d : Int} (hac : a ≤ c) (hbd : b ≤ d) (hb : 0 ≤ b) (hc : 0 ≤ c) :
a * b ≤ c * d
source
theorem Int.mul_le_mul_of_le_of_le_of_nonpos_of_nonpos {a b c d : Int} (hac : c ≤ a) (hbd : d ≤ b) (hb : b ≤ 0) (hc : c ≤ 0) :
a * b ≤ c * d
source
theorem Int.mul_le_mul_of_le_of_le_of_nonpos_of_nonneg {a b c d : Int} (hac : c ≤ a) (hbd : b ≤ d) (hb : b ≤ 0) (hc : 0 ≤ c) :
a * b ≤ c * d
source
theorem Int.neg_mul_le_mul {x y : Int} {s t : Nat} (lbx : -↑s ≤ x) (ubx : x < ↑s) (lby : -↑t ≤ y) (uby : y < ↑t) :
-(↑s * ↑t) ≤ x * y

A corollary of |s| ≤ x, and |t| ≤ y, then |s * t| ≤ x * y,

## pow #

source
theorem Int.natAbs_pow_two (a : Int) :
↑a.natAbs ^ 2 = a ^ 2