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} : Int.NonNeg a ↔ ∃ (n : Nat), a = ↑n

theorem Int.NonNeg.elim {a : Int} : Int.NonNeg a → ∃ (n : Nat), 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 : Nat), b - a = ↑n

theorem Int.le.dest {a : Int} {b : Int} (h : a ≤ b) : ∃ (n : Nat), 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 : Nat), a = ↑n

theorem Int.eq_succ_of_zero_lt {a : Int} (h : 0 < a) : ∃ (n : Nat), 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 : Nat), 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.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.ne_iff_lt_or_gt {a : Int} {b : Int} : a ≠ b ↔ a < b ∨ b < a

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

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

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

instance Int.instTransIntLeInstLEInt : Trans (fun (x x_1 : Int) => x ≤ x_1) (fun (x x_1 : Int) => x ≤ x_1) fun (x x_1 : Int) => x ≤ x_1

Equations

• Int.instTransIntLeInstLEInt = { trans := ⋯ }

instance Int.instTransIntLtInstLTIntLeInstLEInt : Trans (fun (x x_1 : Int) => x < x_1) (fun (x x_1 : Int) => x ≤ x_1) fun (x x_1 : Int) => x < x_1

Equations

• Int.instTransIntLtInstLTIntLeInstLEInt = { trans := ⋯ }

instance Int.instTransIntLeInstLEIntLtInstLTInt : Trans (fun (x x_1 : Int) => x ≤ x_1) (fun (x x_1 : Int) => x < x_1) fun (x x_1 : Int) => x < x_1

Equations

• Int.instTransIntLeInstLEIntLtInstLTInt = { trans := ⋯ }

instance Int.instTransIntLtInstLTInt : Trans (fun (x x_1 : Int) => x < x_1) (fun (x x_1 : Int) => x < x_1) fun (x x_1 : Int) => x < x_1

Equations

• Int.instTransIntLtInstLTInt = { trans := ⋯ }

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.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.le_min {a : Int} {b : Int} {c : Int} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c

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

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

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 : 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_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_left_le_of_le_add {a : Int} {b : Int} {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 : Int} {b : Int} (H : a < b) : a + 1 ≤ b

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.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_le_mul_of_nonpos_right {a : Int} {b : Int} {c : Int} (h : b ≤ a) (hc : c ≤ 0) : a * c ≤ b * c

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

@[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_pos {a : Int} : 0 < Int.natAbs a ↔ a ≠ 0

@[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.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_eq_natAbs_iff {a : Int} {b : Int} : Int.natAbs a = Int.natAbs b ↔ a = b ∨ a = -b

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

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

@[simp]

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