Further lemmas about Int relying on omega automation.

miscellaneous lemmas

@[simp]

theorem Int.natCast_le_zero {n : Nat} : ↑n ≤ 0 ↔ n = 0

@[simp]

theorem Int.neg_nonpos_iff (i : Int) : -i ≤ 0 ↔ 0 ≤ i

@[simp]

theorem Int.zero_le_ofNat (n : Nat) : 0 ≤ OfNat.ofNat n

@[simp]

theorem Int.neg_natCast_le_natCast (n m : Nat) : -↑n ≤ ↑m

@[simp]

theorem Int.neg_natCast_le_ofNat (n m : Nat) : -↑n ≤ OfNat.ofNat m

@[simp]

theorem Int.neg_ofNat_le_ofNat (n m : Nat) : -OfNat.ofNat n ≤ OfNat.ofNat m

@[simp]

theorem Int.neg_ofNat_le_natCast (n m : Nat) : -OfNat.ofNat n ≤ ↑m

theorem Int.neg_lt_self_iff {n : Int} : -n < n ↔ 0 < n

theorem Int.ofNat_add_out (m n : Nat) : ↑m + ↑n = ↑(m + n)

theorem Int.ofNat_mul_out (m n : Nat) : ↑m * ↑n = ↑(m * n)

theorem Int.ofNat_add_one_out (n : Nat) : ↑n + 1 = ↑n.succ

@[simp]

theorem Int.ofNat_eq_natCast (n : Nat) : ofNat n = ↑n

theorem Int.natCast_inj {m n : Nat} : ↑m = ↑n ↔ m = n

@[simp]

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

theorem Int.natCast_sub {n m : Nat} : n ≤ m → ↑(m - n) = ↑m - ↑n

@[simp]

theorem Int.natCast_eq_zero {n : Nat} : ↑n = 0 ↔ n = 0

theorem Int.natCast_ne_zero {n : Nat} : ↑n ≠ 0 ↔ n ≠ 0

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

@[simp]

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

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

@[simp]

theorem Int.natCast_nonpos_iff {n : Nat} : ↑n ≤ 0 ↔ n = 0

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

@[simp]

theorem Int.sign_natCast_add_one (n : Nat) : (↑n + 1).sign = 1

@[simp]

theorem Int.cast_id {n : Int} : ↑n = n

toNat

@[simp]

theorem Int.toNat_sub' (a : Int) (b : Nat) : (a - ↑b).toNat = a.toNat - b

@[simp]

theorem Int.toNat_sub_max_self (a : Int) : (a - max a 0).toNat = 0

@[simp]

theorem Int.toNat_sub_self_max (a : Int) : (a - max 0 a).toNat = 0

@[simp]

theorem Int.toNat_eq_zero {n : Int} : n.toNat = 0 ↔ n ≤ 0

@[simp]

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

@[simp]

theorem Int.toNat_lt' {m : Int} {n : Nat} (hn : 0 < n) : m.toNat < n ↔ m < ↑n

@[simp]

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

theorem Int.lt_of_toNat_lt {a b : Int} (h : a.toNat < b.toNat) : a < b

theorem Int.toNat_sub_of_le {a b : Int} (h : b ≤ a) : ↑(a - b).toNat = a - b

theorem Int.pos_iff_toNat_pos {n : Int} : 0 < n ↔ 0 < n.toNat

theorem Int.natCast_toNat_eq_self {a : Int} : ↑a.toNat = a ↔ 0 ≤ a

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

theorem Int.ofNat_toNat_eq_self {a : Int} : ↑a.toNat = a ↔ 0 ≤ a

theorem Int.eq_natCast_toNat {a : Int} : a = ↑a.toNat ↔ 0 ≤ a

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

theorem Int.eq_ofNat_toNat {a : Int} : a = ↑a.toNat ↔ 0 ≤ a

theorem Int.toNat_le_toNat {n m : Int} (h : n ≤ m) : n.toNat ≤ m.toNat

theorem Int.toNat_lt_toNat {n m : Int} (hn : 0 < m) : n.toNat < m.toNat ↔ n < m

min and max

@[simp]

theorem Int.min_assoc (a b c : Int) : min (min a b) c = min a (min b c)

instance Int.instAssociativeNatMin : Std.Associative min

@[simp]

theorem Int.min_self_assoc {m n : Int} : min m (min m n) = min m n

@[simp]

theorem Int.min_self_assoc' {m n : Int} : min n (min m n) = min n m

@[simp]

theorem Int.max_assoc (a b c : Int) : max (max a b) c = max a (max b c)

instance Int.instAssociativeNatMax : Std.Associative max

@[simp]

theorem Int.max_self_assoc {m n : Int} : max m (max m n) = max m n

@[simp]

theorem Int.max_self_assoc' {m n : Int} : max n (max m n) = max n m

theorem Int.max_min_distrib_left (a b c : Int) : max a (min b c) = min (max a b) (max a c)

theorem Int.min_max_distrib_left (a b c : Int) : min a (max b c) = max (min a b) (min a c)

theorem Int.max_min_distrib_right (a b c : Int) : max (min a b) c = min (max a c) (max b c)

theorem Int.min_max_distrib_right (a b c : Int) : min (max a b) c = max (min a c) (min b c)

theorem Int.sub_min_sub_right (a b c : Int) : min (a - c) (b - c) = min a b - c

theorem Int.sub_max_sub_right (a b c : Int) : max (a - c) (b - c) = max a b - c

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

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

mul

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

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.

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

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

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

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

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