Lemmas about Nat and Int needed internally by omega.

These statements are useful for constructing proof expressions, but unlikely to be widely useful, so are inside the Std.Tactic.Omega namespace.

If you do find a use for them, please move them into the appropriate file and namespace!

theorem Std.Tactic.Omega.Int.natCast_ofNat {x : Nat} : ↑(OfNat.ofNat x) = OfNat.ofNat x

theorem Std.Tactic.Omega.Int.ofNat_lt_of_lt {n : Nat} {m : Nat} : n < m → ↑n < ↑m

Alias of the reverse direction of Int.ofNat_lt.

theorem Std.Tactic.Omega.Int.ofNat_le_of_le {m : Nat} {n : Nat} : m ≤ n → ↑m ≤ ↑n

Alias of the reverse direction of Int.ofNat_le.

theorem Std.Tactic.Omega.Int.lt_of_not_ge {a : Int} {b : Int} : ¬a ≤ b → b < a

Alias of the forward direction of Int.not_le.

theorem Std.Tactic.Omega.Int.not_le_of_lt {a : Int} {b : Int} : b < a → ¬a ≤ b

Alias of the reverse direction of Int.not_le.

theorem Std.Tactic.Omega.Int.lt_of_not_le {a : Int} {b : Int} : ¬a ≤ b → b < a

Alias of the forward direction of Int.not_le.

theorem Std.Tactic.Omega.Int.lt_le_asymm {a : Int} {b : Int} : b < a → ¬a ≤ b

Alias of the reverse direction of Int.not_le.

theorem Std.Tactic.Omega.Int.not_lt_of_ge {a : Int} {b : Int} : b ≤ a → ¬a < b

Alias of the reverse direction of Int.not_lt.

theorem Std.Tactic.Omega.Int.le_of_not_gt {a : Int} {b : Int} : ¬a < b → b ≤ a

Alias of the forward direction of Int.not_lt.

theorem Std.Tactic.Omega.Int.le_of_not_lt {a : Int} {b : Int} : ¬a < b → b ≤ a

Alias of the forward direction of Int.not_lt.

theorem Std.Tactic.Omega.Int.not_lt_of_le {a : Int} {b : Int} : b ≤ a → ¬a < b

Alias of the reverse direction of Int.not_lt.

theorem Std.Tactic.Omega.Int.le_lt_asymm {a : Int} {b : Int} : b ≤ a → ¬a < b

Alias of the reverse direction of Int.not_lt.

theorem Std.Tactic.Omega.Int.add_congr {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a = b) (h₂ : c = d) : a + c = b + d

theorem Std.Tactic.Omega.Int.mul_congr {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a = b) (h₂ : c = d) : a * c = b * d

theorem Std.Tactic.Omega.Int.mul_congr_left {a : Int} {b : Int} (h₁ : a = b) (c : Int) : a * c = b * c

theorem Std.Tactic.Omega.Int.sub_congr {a : Int} {b : Int} {c : Int} {d : Int} (h₁ : a = b) (h₂ : c = d) : a - c = b - d

theorem Std.Tactic.Omega.Int.neg_congr {a : Int} {b : Int} (h₁ : a = b) : -a = -b

theorem Std.Tactic.Omega.Int.lt_of_gt {x : Int} {y : Int} (h : x > y) : y < x

theorem Std.Tactic.Omega.Int.le_of_ge {x : Int} {y : Int} (h : x ≥ y) : y ≤ x

theorem Std.Tactic.Omega.Int.ofNat_sub_eq_zero {b : Nat} {a : Nat} (h : ¬b ≤ a) : ↑(a - b) = 0

theorem Std.Tactic.Omega.Int.ofNat_sub_dichotomy {a : Nat} {b : Nat} : b ≤ a ∧ ↑(a - b) = ↑a - ↑b ∨ a < b ∧ ↑(a - b) = 0

theorem Std.Tactic.Omega.Int.ofNat_congr {a : Nat} {b : Nat} (h : a = b) : ↑a = ↑b

theorem Std.Tactic.Omega.Int.ofNat_sub_sub {a : Nat} {b : Nat} {c : Nat} : ↑(a - b - c) = ↑(a - (b + c))

theorem Std.Tactic.Omega.Int.natAbs_dichotomy {a : Int} : 0 ≤ a ∧ ↑(Int.natAbs a) = a ∨ a < 0 ∧ ↑(Int.natAbs a) = -a

theorem Std.Tactic.Omega.Int.add_le_iff_le_sub (a : Int) (b : Int) (c : Int) : a + b ≤ c ↔ a ≤ c - b

theorem Std.Tactic.Omega.Int.le_add_iff_sub_le (a : Int) (b : Int) (c : Int) : a ≤ b + c ↔ a - c ≤ b

theorem Std.Tactic.Omega.Int.add_le_zero_iff_le_neg (a : Int) (b : Int) : a + b ≤ 0 ↔ a ≤ -b

theorem Std.Tactic.Omega.Int.add_le_zero_iff_le_neg' (a : Int) (b : Int) : a + b ≤ 0 ↔ b ≤ -a

theorem Std.Tactic.Omega.Int.add_nonnneg_iff_neg_le (a : Int) (b : Int) : 0 ≤ a + b ↔ -b ≤ a

theorem Std.Tactic.Omega.Int.add_nonnneg_iff_neg_le' (a : Int) (b : Int) : 0 ≤ a + b ↔ -a ≤ b

theorem Std.Tactic.Omega.Int.ofNat_fst_mk {β : Type u_1} {x : Nat} {y : β} : ↑(x, y).fst = ↑x

theorem Std.Tactic.Omega.Int.ofNat_snd_mk {α : Type u_1} {x : α} {y : Nat} : ↑(x, y).snd = ↑y

theorem Std.Tactic.Omega.Nat.lt_of_gt {x : Nat} {y : Nat} (h : x > y) : y < x

theorem Std.Tactic.Omega.Nat.le_of_ge {x : Nat} {y : Nat} (h : x ≥ y) : y ≤ x

theorem Std.Tactic.Omega.Prod.of_lex : ∀ {α : Type u_1} {r : α → α → Prop} {β : Type u_2} {s : β → β → Prop} {p q : α × β}, Prod.Lex r s p q → r p.fst q.fst ∨ p.fst = q.fst ∧ s p.snd q.snd

theorem Std.Tactic.Omega.Prod.of_not_lex {α : Type u_1} {r : α → α → Prop} [DecidableEq α] {β : Type u_2} {s : β → β → Prop} {p : α × β} {q : α × β} (w : ¬Prod.Lex r s p q) : ¬r p.fst q.fst ∧ (p.fst ≠ q.fst ∨ ¬s p.snd q.snd)

theorem Std.Tactic.Omega.Prod.fst_mk : ∀ {α : Type u_1} {x : α} {β : Type u_2} {y : β}, (x, y).fst = x

theorem Std.Tactic.Omega.Prod.snd_mk : ∀ {α : Type u_1} {x : α} {α_1 : Type u_2} {y : α_1}, (x, y).snd = y