@[simp]

theorem Int.ofNat_eq_coe {n : Nat} : Int.ofNat n = ↑n

@[simp]

theorem Int.ofNat_zero : ↑0 = 0

@[simp]

theorem Int.ofNat_one : ↑1 = 1

@[simp]

theorem Int.default_eq_zero : default = 0

theorem Int.subNatNat_of_sub_eq_zero {m : Nat} {n : Nat} (h : n - m = 0) : Int.subNatNat m n = ↑(m - n)

theorem Int.subNatNat_of_sub_eq_succ {m : Nat} {n : Nat} {k : Nat} (h : n - m = Nat.succ k) : Int.subNatNat m n = Int.negSucc k

theorem Int.neg_zero : -0 = 0

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

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

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

theorem Int.neg_ofNat_zero : -↑0 = 0

theorem Int.neg_ofNat_succ (n : Nat) : -↑(Nat.succ n) = Int.negSucc n

theorem Int.neg_negSucc (n : Nat) : -Int.negSucc n = ↑(Nat.succ n)

theorem Int.negSucc_coe (n : Nat) : Int.negSucc n = -↑(n + 1)

theorem Int.negOfNat_eq {n : Nat} : Int.negOfNat n = -Int.ofNat n

@[simp]

theorem Int.add_def {a : Int} {b : Int} : Int.add a b = a + b

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

theorem Int.ofNat_add_negSucc (m : Nat) (n : Nat) : ↑m + Int.negSucc n = Int.subNatNat m (Nat.succ n)

theorem Int.negSucc_add_ofNat (m : Nat) (n : Nat) : Int.negSucc m + ↑n = Int.subNatNat n (Nat.succ m)

theorem Int.negSucc_add_negSucc (m : Nat) (n : Nat) : Int.negSucc m + Int.negSucc n = Int.negSucc (Nat.succ (m + n))

@[simp]

theorem Int.mul_def {a : Int} {b : Int} : Int.mul a b = a * b

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

theorem Int.ofNat_mul_negSucc' (m : Nat) (n : Nat) : ↑m * Int.negSucc n = Int.negOfNat (m * Nat.succ n)

theorem Int.negSucc_mul_ofNat' (m : Nat) (n : Nat) : Int.negSucc m * ↑n = Int.negOfNat (Nat.succ m * n)

theorem Int.negSucc_mul_negSucc' (m : Nat) (n : Nat) : Int.negSucc m * Int.negSucc n = Int.ofNat (Nat.succ m * Nat.succ n)

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

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

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

theorem Int.negSucc_inj {m : Nat} {n : Nat} : Int.negSucc m = Int.negSucc n ↔ m = n

theorem Int.negSucc_eq (n : Nat) : Int.negSucc n = -(↑n + 1)

@[simp]

theorem Int.negSucc_ne_zero (n : Nat) : Int.negSucc n ≠ 0

@[simp]

theorem Int.zero_ne_negSucc (n : Nat) : 0 ≠ Int.negSucc n

@[simp]

theorem Int.neg_neg (a : Int) : - -a = a

theorem Int.neg_inj {a : Int} {b : Int} : -a = -b ↔ a = b

theorem Int.neg_eq_zero {a : Int} : -a = 0 ↔ a = 0

theorem Int.neg_ne_zero {a : Int} : -a ≠ 0 ↔ a ≠ 0

theorem Int.sub_eq_add_neg {a : Int} {b : Int} : a - b = a + -b

theorem Int.add_neg_one (i : Int) : i + -1 = i - 1

theorem Int.subNatNat_elim (m : Nat) (n : Nat) (motive : Nat → Nat → Int → Prop) (hp : (i n : Nat) → motive (n + i) n ↑i) (hn : (i m : Nat) → motive m (m + i + 1) (Int.negSucc i)) : motive m n (Int.subNatNat m n)

theorem Int.subNatNat_add_left {m : Nat} {n : Nat} : Int.subNatNat (m + n) m = ↑n

theorem Int.subNatNat_add_right {m : Nat} {n : Nat} : Int.subNatNat m (m + n + 1) = Int.negSucc n

theorem Int.subNatNat_add_add (m : Nat) (n : Nat) (k : Nat) : Int.subNatNat (m + k) (n + k) = Int.subNatNat m n

theorem Int.subNatNat_of_le {m : Nat} {n : Nat} (h : n ≤ m) : Int.subNatNat m n = ↑(m - n)

theorem Int.subNatNat_of_lt {m : Nat} {n : Nat} (h : m < n) : Int.subNatNat m n = Int.negSucc (Nat.pred (n - m))

@[simp]

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

@[simp]

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

@[simp]

theorem Int.natAbs_zero : Int.natAbs 0 = 0

@[simp]

theorem Int.natAbs_one : Int.natAbs 1 = 1

@[simp]

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

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

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

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

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

@[simp]

theorem Int.sign_zero : Int.sign 0 = 0

@[simp]

theorem Int.sign_one : Int.sign 1 = 1

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

theorem Int.sign_of_succ (n : Nat) : Int.sign ↑(Nat.succ n) = 1

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

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

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

@[simp]

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

theorem Int.add_comm (a : Int) (b : Int) : a + b = b + a

theorem Int.add_zero (a : Int) : a + 0 = a

theorem Int.zero_add (a : Int) : 0 + a = a

theorem Int.ofNat_add_negSucc_of_lt {m : Nat} {n : Nat} (h : m < Nat.succ n) : Int.ofNat m + Int.negSucc n = Int.negSucc (n - m)

theorem Int.subNatNat_sub {n : Nat} {m : Nat} (h : n ≤ m) (k : Nat) : Int.subNatNat (m - n) k = Int.subNatNat m (k + n)

theorem Int.subNatNat_add (m : Nat) (n : Nat) (k : Nat) : Int.subNatNat (m + n) k = ↑m + Int.subNatNat n k

theorem Int.subNatNat_add_negSucc (m : Nat) (n : Nat) (k : Nat) : Int.subNatNat m n + Int.negSucc k = Int.subNatNat m (n + Nat.succ k)

theorem Int.add_assoc (a : Int) (b : Int) (c : Int) : a + b + c = a + (b + c)

theorem Int.add_assoc.aux1 (m : Nat) (n : Nat) (c : Int) : ↑m + ↑n + c = ↑m + (↑n + c)

theorem Int.add_assoc.aux2 (m : Nat) (n : Nat) (k : Nat) : Int.negSucc m + Int.negSucc n + ↑k = Int.negSucc m + (Int.negSucc n + ↑k)

theorem Int.add_left_comm (a : Int) (b : Int) (c : Int) : a + (b + c) = b + (a + c)

theorem Int.add_right_comm (a : Int) (b : Int) (c : Int) : a + b + c = a + c + b

theorem Int.subNatNat_self (n : Nat) : Int.subNatNat n n = 0

theorem Int.add_left_neg (a : Int) : -a + a = 0

theorem Int.add_right_neg (a : Int) : a + -a = 0

@[simp]

theorem Int.neg_eq_of_add_eq_zero {a : Int} {b : Int} (h : a + b = 0) : -a = b

theorem Int.eq_neg_of_eq_neg {a : Int} {b : Int} (h : a = -b) : b = -a

theorem Int.eq_neg_comm {a : Int} {b : Int} : a = -b ↔ b = -a

theorem Int.neg_eq_comm {a : Int} {b : Int} : -a = b ↔ -b = a

theorem Int.neg_add_cancel_left (a : Int) (b : Int) : -a + (a + b) = b

theorem Int.add_neg_cancel_left (a : Int) (b : Int) : a + (-a + b) = b

theorem Int.add_neg_cancel_right (a : Int) (b : Int) : a + b + -b = a

theorem Int.neg_add_cancel_right (a : Int) (b : Int) : a + -b + b = a

theorem Int.add_left_cancel {a : Int} {b : Int} {c : Int} (h : a + b = a + c) : b = c

theorem Int.neg_add {a : Int} {b : Int} : -(a + b) = -a + -b

@[simp]

theorem Int.negSucc_sub_one (n : Nat) : Int.negSucc n - 1 = Int.negSucc (n + 1)

theorem Int.sub_self (a : Int) : a - a = 0

theorem Int.sub_zero (a : Int) : a - 0 = a

theorem Int.zero_sub (a : Int) : 0 - a = -a

theorem Int.sub_eq_zero_of_eq {a : Int} {b : Int} (h : a = b) : a - b = 0

theorem Int.eq_of_sub_eq_zero {a : Int} {b : Int} (h : a - b = 0) : a = b

theorem Int.sub_eq_zero {a : Int} {b : Int} : a - b = 0 ↔ a = b

theorem Int.sub_sub (a : Int) (b : Int) (c : Int) : a - b - c = a - (b + c)

theorem Int.neg_sub (a : Int) (b : Int) : -(a - b) = b - a

theorem Int.sub_sub_self (a : Int) (b : Int) : a - (a - b) = b

theorem Int.sub_neg (a : Int) (b : Int) : a - -b = a + b

@[simp]

theorem Int.ofNat_mul_negSucc (m : Nat) (n : Nat) : ↑m * Int.negSucc n = -↑(m * Nat.succ n)

@[simp]

theorem Int.negSucc_mul_ofNat (m : Nat) (n : Nat) : Int.negSucc m * ↑n = -↑(Nat.succ m * n)

@[simp]

theorem Int.negSucc_mul_negSucc (m : Nat) (n : Nat) : Int.negSucc m * Int.negSucc n = ↑(Nat.succ m) * ↑(Nat.succ n)

theorem Int.mul_comm (a : Int) (b : Int) : a * b = b * a

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

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

theorem Int.negSucc_mul_negOfNat (m : Nat) (n : Nat) : Int.negSucc m * Int.negOfNat n = Int.ofNat (Nat.succ m * n)

theorem Int.negOfNat_mul_negSucc (m : Nat) (n : Nat) : Int.negOfNat n * Int.negSucc m = Int.ofNat (n * Nat.succ m)

theorem Int.mul_assoc (a : Int) (b : Int) (c : Int) : a * b * c = a * (b * c)

theorem Int.mul_left_comm (a : Int) (b : Int) (c : Int) : a * (b * c) = b * (a * c)

theorem Int.mul_right_comm (a : Int) (b : Int) (c : Int) : a * b * c = a * c * b

@[simp]

theorem Int.mul_zero (a : Int) : a * 0 = 0

@[simp]

theorem Int.zero_mul (a : Int) : 0 * a = 0

theorem Int.negOfNat_eq_subNatNat_zero (n : Nat) : Int.negOfNat n = Int.subNatNat 0 n

theorem Int.ofNat_mul_subNatNat (m : Nat) (n : Nat) (k : Nat) : ↑m * Int.subNatNat n k = Int.subNatNat (m * n) (m * k)

theorem Int.negOfNat_add (m : Nat) (n : Nat) : Int.negOfNat m + Int.negOfNat n = Int.negOfNat (m + n)

theorem Int.negSucc_mul_subNatNat (m : Nat) (n : Nat) (k : Nat) : Int.negSucc m * Int.subNatNat n k = Int.subNatNat (Nat.succ m * k) (Nat.succ m * n)

theorem Int.mul_add (a : Int) (b : Int) (c : Int) : a * (b + c) = a * b + a * c

theorem Int.add_mul (a : Int) (b : Int) (c : Int) : (a + b) * c = a * c + b * c

theorem Int.neg_mul_eq_neg_mul (a : Int) (b : Int) : -(a * b) = -a * b

theorem Int.neg_mul_eq_mul_neg (a : Int) (b : Int) : -(a * b) = a * -b

theorem Int.neg_mul (a : Int) (b : Int) : -a * b = -(a * b)

theorem Int.mul_neg (a : Int) (b : Int) : a * -b = -(a * b)

theorem Int.neg_mul_neg (a : Int) (b : Int) : -a * -b = a * b

theorem Int.neg_mul_comm (a : Int) (b : Int) : -a * b = a * -b

theorem Int.mul_sub (a : Int) (b : Int) (c : Int) : a * (b - c) = a * b - a * c

theorem Int.sub_mul (a : Int) (b : Int) (c : Int) : (a - b) * c = a * c - b * c

theorem Int.zero_ne_one : 0 ≠ 1

@[simp]

theorem Int.sub_add_cancel (a : Int) (b : Int) : a - b + b = a

@[simp]

theorem Int.add_sub_cancel (a : Int) (b : Int) : a + b - b = a

theorem Int.add_sub_assoc (a : Int) (b : Int) (c : Int) : a + b - c = a + (b - c)

theorem Int.ofNat_sub {m : Nat} {n : Nat} (h : m ≤ n) : ↑(n - m) = ↑n - ↑m

theorem Int.negSucc_coe' (n : Nat) : Int.negSucc n = -↑n - 1

theorem Int.subNatNat_eq_coe {m : Nat} {n : Nat} : Int.subNatNat m n = ↑m - ↑n

theorem Int.toNat_sub (m : Nat) (n : Nat) : Int.toNat (↑m - ↑n) = m - n

@[simp]

theorem Int.one_mul (a : Int) : 1 * a = a

@[simp]

theorem Int.mul_one (a : Int) : a * 1 = a

theorem Int.mul_neg_one (a : Int) : a * -1 = -a

theorem Int.neg_eq_neg_one_mul (a : Int) : -a = -1 * a

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

@[simp]

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

Order properties of the integers

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

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

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

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

theorem Int.lt_iff_add_one_le (a : Int) (b : Int) : a < b ↔ a + 1 ≤ b

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

theorem Int.zero_lt_one : 0 < 1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Int.add_lt_add_of_lt_of_le {a : Int} {b : Int} {c : Int} {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 : Int} {b : Int} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ a + b

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

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

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

theorem Int.nonpos_of_neg_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 : Int} {b : Int} (h : a < b) : -b < -a

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Int.sub_lt_sub_of_lt_of_le {a : Int} {b : Int} {c : Int} {d : Int} (hab : a < b) (hcd : c ≤ d) : a - d < 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_le_add_three {a : Int} {b : Int} {c : Int} {d : Int} {e : Int} {f : Int} (h₁ : a ≤ d) (h₂ : b ≤ e) (h₃ : c ≤ f) : a + b + c ≤ d + e + f

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

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

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

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

theorem Int.mul_le_mul {a : Int} {b : Int} {c : Int} {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 : Int} {b : Int} (ha : 0 ≤ a) (hb : b ≤ 0) : a * b ≤ 0

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

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

theorem Int.mul_lt_mul' {a : Int} {b : Int} {c : Int} {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 : Int} {b : Int} (ha : 0 < a) (hb : b < 0) : a * b < 0

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Int.sign_eq_one_iff_pos (a : Int) : Int.sign a = 1 ↔ 0 < a

theorem Int.sign_eq_neg_one_iff_neg (a : Int) : Int.sign a = -1 ↔ a < 0

theorem Int.sign_eq_zero_iff_zero (a : Int) : Int.sign a = 0 ↔ a = 0

theorem Int.mul_eq_zero {a : Int} {b : Int} : a * b = 0 ↔ a = 0 ∨ b = 0

theorem Int.mul_ne_zero {a : Int} {b : Int} (a0 : a ≠ 0) (b0 : b ≠ 0) : a * b ≠ 0

theorem Int.eq_of_mul_eq_mul_right {a : Int} {b : Int} {c : Int} (ha : a ≠ 0) (h : b * a = c * a) : b = c

theorem Int.eq_of_mul_eq_mul_left {a : Int} {b : Int} {c : Int} (ha : a ≠ 0) (h : a * b = a * c) : b = c

theorem Int.eq_one_of_mul_eq_self_left {a : Int} {b : Int} (Hpos : a ≠ 0) (H : b * a = a) : b = 1

theorem Int.eq_one_of_mul_eq_self_right {a : Int} {b : Int} (Hpos : b ≠ 0) (H : b * a = b) : a = 1

nat abs

theorem Int.ofNat_natAbs_eq_of_nonneg (a : Int) : 0 ≤ a → ↑(Int.natAbs a) = a

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

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

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

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

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

toNat

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

@[simp]

theorem Int.toNat_zero : Int.toNat 0 = 0

@[simp]

theorem Int.toNat_one : Int.toNat 1 = 1

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem Int.mem_toNat' (a : Int) (n : Nat) : Int.toNat' a = some n ↔ a = ↑n

@[simp]

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

The following lemmas are later subsumed by e.g. Nat.cast_add and Nat.cast_mul in Mathlib but it is convenient to have these earlier, for users who only need Nat and Int.

theorem Int.natCast_zero : ↑0 = 0

theorem Int.natCast_one : ↑1 = 1

@[simp]

theorem Int.natCast_add (a : Nat) (b : Nat) : ↑(a + b) = ↑a + ↑b

@[simp]

theorem Int.natCast_mul (a : Nat) (b : Nat) : ↑(a * b) = ↑a * ↑b