Documentation

Init.Data.Int.LemmasAux

Further lemmas about Int relying on omega automation. #

miscellaneous lemmas #

source
@[simp]
theorem Int.natCast_le_zero {n : Nat} :
↑n ≤ 0 ↔ n = 0
source
theorem Int.sub_eq_iff_eq_add {b a c : Int} :
a - b = c ↔ a = c + b
source
theorem Int.sub_eq_iff_eq_add' {b a c : Int} :
a - b = c ↔ a = b + c
source
@[simp]
theorem Int.neg_nonpos_iff (i : Int) :
-i ≤ 0 ↔ 0 ≤ i
source
@[simp]
theorem Int.zero_le_ofNat (n : Nat) :
0 ≤ OfNat.ofNat n
source
@[simp]
theorem Int.neg_natCast_le_natCast (n m : Nat) :
-↑n ≤ ↑m
source
@[simp]
theorem Int.neg_natCast_le_ofNat (n m : Nat) :
-↑n ≤ OfNat.ofNat m
source
@[simp]
theorem Int.neg_ofNat_le_ofNat (n m : Nat) :
-OfNat.ofNat n ≤ OfNat.ofNat m
source
@[simp]
theorem Int.neg_ofNat_le_natCast (n m : Nat) :
-OfNat.ofNat n ≤ ↑m
source
theorem Int.neg_lt_self_iff {n : Int} :
-n < n ↔ 0 < n

toNat #

source
@[simp]
theorem Int.toNat_sub' (a : Int) (b : Nat) :
(a - ↑b).toNat = a.toNat - b
source
@[simp]
theorem Int.toNat_sub_max_self (a : Int) :
(a - max a 0).toNat = 0
source
@[simp]
theorem Int.toNat_sub_self_max (a : Int) :
(a - max 0 a).toNat = 0
source
@[simp]
theorem Int.toNat_eq_zero {n : Int} :
n.toNat = 0 ↔ n ≤ 0
source
@[simp]
theorem Int.toNat_le {m : Int} {n : Nat} :
m.toNat ≤ n ↔ m ≤ ↑n
source
@[simp]
theorem Int.toNat_lt' {m : Int} {n : Nat} (hn : 0 < n) :
m.toNat < n ↔ m < ↑n
source
theorem Int.pos_iff_toNat_pos {n : Int} :
0 < n ↔ 0 < n.toNat
source
theorem Int.ofNat_toNat_eq_self {a : Int} :
↑a.toNat = a ↔ 0 ≤ a
source
theorem Int.eq_ofNat_toNat {a : Int} :
a = ↑a.toNat ↔ 0 ≤ a
source
theorem Int.toNat_le_toNat {n m : Int} (h : n ≤ m) :
n.toNat ≤ m.toNat
source
theorem Int.toNat_lt_toNat {n m : Int} (hn : 0 < m) :
n.toNat < m.toNat ↔ n < m

natAbs #

source
theorem Int.eq_zero_of_dvd_of_natAbs_lt_natAbs {d n : Int} (h : d ∣ n) (h₁ : n.natAbs < d.natAbs) :
n = 0

min and max #

source
@[simp]
theorem Int.min_assoc (a b c : Int) :
min (min a b) c = min a (min b c)
source
instance Int.instAssociativeNatMin :
Std.Associative min
source
@[simp]
theorem Int.min_self_assoc {m n : Int} :
min m (min m n) = min m n
source
@[simp]
theorem Int.min_self_assoc' {m n : Int} :
min n (min m n) = min n m
source
@[simp]
theorem Int.max_assoc (a b c : Int) :
max (max a b) c = max a (max b c)
source
instance Int.instAssociativeNatMax :
Std.Associative max
source
@[simp]
theorem Int.max_self_assoc {m n : Int} :
max m (max m n) = max m n
source
@[simp]
theorem Int.max_self_assoc' {m n : Int} :
max n (max m n) = max n m
source
theorem Int.max_min_distrib_left (a b c : Int) :
max a (min b c) = min (max a b) (max a c)
source
theorem Int.min_max_distrib_left (a b c : Int) :
min a (max b c) = max (min a b) (min a c)
source
theorem Int.max_min_distrib_right (a b c : Int) :
max (min a b) c = min (max a c) (max b c)
source
theorem Int.min_max_distrib_right (a b c : Int) :
min (max a b) c = max (min a c) (min b c)
source
theorem Int.sub_min_sub_right (a b c : Int) :
min (a - c) (b - c) = min a b - c
source
theorem Int.sub_max_sub_right (a b c : Int) :
max (a - c) (b - c) = max a b - c
source
theorem Int.sub_min_sub_left (a b c : Int) :
min (a - b) (a - c) = a - max b c
source
theorem Int.sub_max_sub_left (a b c : Int) :
max (a - b) (a - c) = a - min b c

bmod #

source
theorem Int.bmod_neg_iff {m : Nat} {x : Int} (h2 : -↑m ≤ x) (h1 : x < ↑m) :
x.bmod m < 0 ↔ -(↑m / 2) ≤ x ∧ x < 0 ∨ (↑m + 1) / 2 ≤ x
source
theorem Int.bmod_eq_self_of_le {n : Int} {m : Nat} (hn' : -(↑m / 2) ≤ n) (hn : n < (↑m + 1) / 2) :
n.bmod m = n
source
theorem Int.bmod_bmod_of_dvd {a : Int} {n m : Nat} (hnm : n ∣ m) :
(a.bmod m).bmod n = a.bmod n