Lemmas about Nat, Int, and Fin needed internally by omega.

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

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

theorem Lean.Omega.Int.ofNat_pow (a b : Nat) : ↑(a ^ b) = ↑a ^ b

theorem Lean.Omega.Int.pos_pow_of_pos (a : Int) (b : Nat) (h : 0 < a) : 0 < a ^ b

theorem Lean.Omega.Int.ofNat_pos {a : Nat} : 0 < ↑a ↔ 0 < a

theorem Lean.Omega.Int.ofNat_pos_of_pos {a : Nat} (h : 0 < a) : 0 < ↑a

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

theorem Lean.Omega.Int.ofNat_lt_of_lt {x y : Nat} (h : x < y) : ↑x < ↑y

theorem Lean.Omega.Int.ofNat_le_of_le {x y : Nat} (h : x ≤ y) : ↑x ≤ ↑y

theorem Lean.Omega.Int.ofNat_shiftLeft_eq {x y : Nat} : ↑(x <<< y) = ↑x * ↑(2 ^ y)

theorem Lean.Omega.Int.ofNat_shiftRight_eq_div_pow {x y : Nat} : ↑(x >>> y) = ↑x / ↑(2 ^ y)

theorem Lean.Omega.Int.emod_ofNat_nonneg {x : Nat} {y : Int} : 0 ≤ ↑x % y

theorem Lean.Omega.Int.lt_of_not_ge {x y : Int} (h : ¬x ≤ y) : y < x

theorem Lean.Omega.Int.lt_of_not_le {x y : Int} (h : ¬x ≤ y) : y < x

theorem Lean.Omega.Int.not_le_of_lt {x y : Int} (h : y < x) : ¬x ≤ y

theorem Lean.Omega.Int.lt_le_asymm {x y : Int} (h₁ : y < x) (h₂ : x ≤ y) : False

theorem Lean.Omega.Int.le_lt_asymm {x y : Int} (h₁ : y ≤ x) (h₂ : x < y) : False

theorem Lean.Omega.Int.le_of_not_gt {x y : Int} (h : ¬y > x) : y ≤ x

theorem Lean.Omega.Int.not_lt_of_ge {x y : Int} (h : y ≥ x) : ¬y < x

theorem Lean.Omega.Int.le_of_not_lt {x y : Int} (h : ¬x < y) : y ≤ x

theorem Lean.Omega.Int.not_lt_of_le {x y : Int} (h : y ≤ x) : ¬x < y

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

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

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

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

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

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

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

theorem Lean.Omega.Int.ofNat_mul_nonneg {a b : Nat} : 0 ≤ ↑a * ↑b

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

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

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

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

theorem Lean.Omega.Int.ofNat_min (a b : Nat) : ↑(min a b) = min ↑a ↑b

theorem Lean.Omega.Int.ofNat_max (a b : Nat) : ↑(max a b) = max ↑a ↑b

theorem Lean.Omega.Int.ofNat_natAbs (a : Int) : ↑a.natAbs = if 0 ≤ a then a else -a

theorem Lean.Omega.Int.natAbs_dichotomy {a : Int} : 0 ≤ a ∧ ↑a.natAbs = a ∨ a < 0 ∧ ↑a.natAbs = -a

theorem Lean.Omega.Int.neg_le_natAbs {a : Int} : -a ≤ ↑a.natAbs

theorem Lean.Omega.Int.add_le_iff_le_sub {a b c : Int} : a + b ≤ c ↔ a ≤ c - b

theorem Lean.Omega.Int.le_add_iff_sub_le {a b c : Int} : a ≤ b + c ↔ a - c ≤ b

theorem Lean.Omega.Int.add_le_zero_iff_le_neg {a b : Int} : a + b ≤ 0 ↔ a ≤ -b

theorem Lean.Omega.Int.add_le_zero_iff_le_neg' {a b : Int} : a + b ≤ 0 ↔ b ≤ -a

theorem Lean.Omega.Int.add_nonnneg_iff_neg_le {a b : Int} : 0 ≤ a + b ↔ -b ≤ a

theorem Lean.Omega.Int.add_nonnneg_iff_neg_le' {a b : Int} : 0 ≤ a + b ↔ -a ≤ b

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

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

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

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

theorem Lean.Omega.Fin.ne_iff_lt_or_gt {n : Nat} {i j : Fin n} : i ≠ j ↔ i < j ∨ i > j

theorem Lean.Omega.Fin.lt_or_gt_of_ne {n : Nat} {i j : Fin n} (h : i ≠ j) : i < j ∨ i > j

theorem Lean.Omega.Fin.not_le {n : Nat} {i j : Fin n} : ¬i ≤ j ↔ j < i

theorem Lean.Omega.Fin.not_lt {n : Nat} {i j : Fin n} : ¬i < j ↔ j ≤ i

theorem Lean.Omega.Fin.lt_of_not_le {n : Nat} {i j : Fin n} (h : ¬i ≤ j) : j < i

theorem Lean.Omega.Fin.le_of_not_lt {n : Nat} {i j : Fin n} (h : ¬i < j) : j ≤ i

theorem Lean.Omega.Fin.ofNat_val_add {n : Nat} {x y : Fin n} : ↑↑(x + y) = (↑↑x + ↑↑y) % ↑n

theorem Lean.Omega.Fin.ofNat_val_sub {n : Nat} {x y : Fin n} : ↑↑(x - y) = (↑(n - ↑y) + ↑↑x) % ↑n

theorem Lean.Omega.Fin.ofNat_val_mul {n : Nat} {x y : Fin n} : ↑↑(x * y) = ↑↑x * ↑↑y % ↑n

theorem Lean.Omega.Fin.ofNat_val_natCast {n x y : Nat} (h : y = x % (n + 1)) : ↑↑(OfNat.ofNat x) = OfNat.ofNat y

theorem Lean.Omega.Prod.of_lex {α✝ : Type u_1} {r : α✝ → α✝ → Prop} {β✝ : 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 Lean.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 Lean.Omega.Prod.fst_mk {α✝ : Type u_1} {x : α✝} {β✝ : Type u_2} {y : β✝} : (x, y).fst = x

theorem Lean.Omega.Prod.snd_mk {α✝ : Type u_1} {x : α✝} {α✝¹ : Type u_2} {y : α✝¹} : (x, y).snd = y