# Documentation

Std.Data.Int.Lemmas

@[simp]
theorem Int.ofNat_eq_coe {n : Nat} :
= 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) :
= (m - n)
theorem Int.subNatNat_of_sub_eq_succ {m : Nat} {n : Nat} {k : Nat} (h : n - m = ) :
@[simp]
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) :
() = n + 1
theorem Int.neg_ofNat_succ (n : Nat) :
-() =
theorem Int.neg_negSucc (n : Nat) :
= ()
theorem Int.negSucc_coe (n : Nat) :
= -(n + 1)
theorem Int.negOfNat_eq {n : Nat} :
@[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 + =
theorem Int.negSucc_add_ofNat (m : Nat) (n : Nat) :
+ 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.negOfNat (m * )
theorem Int.negSucc_mul_ofNat' (m : Nat) (n : Nat) :
* n = Int.negOfNat ( * 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} :
m = n
theorem Int.negSucc_eq (n : Nat) :
= -(n + 1)
@[simp]
theorem Int.negSucc_ne_zero (n : Nat) :
0
@[simp]
theorem Int.zero_ne_negSucc (n : Nat) :
0
@[simp]
theorem Int.Nat.cast_ofNat_Int {n : Nat} :
() =
@[simp]
theorem Int.neg_neg (a : Int) :
- -a = a
theorem Int.neg_inj {a : Int} {b : Int} :
-a = -b a = b
@[simp]
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 : NatNat) (hp : ∀ (i n : Nat), motive (n + i) n i) (hn : ∀ (i m : Nat), motive m (m + i + 1) ()) :
motive 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) =
theorem Int.subNatNat_add_add (m : Nat) (n : Nat) (k : Nat) :
Int.subNatNat (m + k) (n + k) =
theorem Int.subNatNat_of_le {m : Nat} {n : Nat} (h : n m) :
= (m - n)
theorem Int.subNatNat_of_lt {m : Nat} {n : Nat} (h : m < n) :
@[simp]
theorem Int.natAbs_ofNat (n : Nat) :
= n
@[simp]
theorem Int.natAbs_negSucc (n : Nat) :
@[simp]
theorem Int.natAbs_zero :
= 0
@[simp]
theorem Int.natAbs_one :
= 1
@[simp]
theorem Int.natAbs_eq_zero {a : Int} :
= 0 a = 0
theorem Int.natAbs_ne_zero {a : Int} :
0 a 0
theorem Int.natAbs_pos {a : Int} :
0 < a 0
theorem Int.natAbs_mul_self {a : Int} :
() = a * a
@[simp]
theorem Int.natAbs_neg (a : Int) :
theorem Int.natAbs_eq (a : Int) :
a = () a = -()
theorem Int.eq_nat_or_neg (a : Int) :
∃ (n : Nat), a = n a = -n
theorem Int.natAbs_negOfNat (n : Nat) :
= n
theorem Int.natAbs_mul (a : Int) (b : Int) :
Int.natAbs (a * b) =
theorem Int.natAbs_mul_natAbs_eq {a : Int} {b : Int} {c : Nat} (h : a * b = c) :
= c
@[simp]
theorem Int.natAbs_mul_self' (a : Int) :
() * () = a * a
theorem Int.natAbs_eq_natAbs_iff {a : Int} {b : Int} :
a = b a = -b
theorem Int.natAbs_eq_iff {a : Int} {n : Nat} :
= n a = n a = -n
@[simp]
theorem Int.sign_zero :
= 0
@[simp]
theorem Int.sign_one :
= 1
theorem Int.sign_of_succ (n : Nat) :
Int.sign () = 1
theorem Int.natAbs_sign (z : Int) :
= if z = 0 then 0 else 1
theorem Int.natAbs_sign_of_nonzero {z : Int} (hz : z 0) :
= 1
theorem Int.sign_ofNat_of_nonzero {n : Nat} (hn : n 0) :
Int.sign n = 1
@[simp]
theorem Int.sign_neg (z : Int) :
theorem Int.add_comm (a : Int) (b : Int) :
a + b = b + a
@[simp]
theorem Int.add_zero (a : Int) :
a + 0 = a
@[simp]
theorem Int.zero_add (a : Int) :
0 + a = a
theorem Int.ofNat_add_negSucc_of_lt {m : Nat} {n : Nat} (h : m < ) :
= 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 +
theorem Int.subNatNat_add_negSucc (m : Nat) (n : Nat) (k : Nat) :
= Int.subNatNat m (n + )
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) :
+ k = + ( + 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) :
= 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) :
- 1 = Int.negSucc (n + 1)
@[simp]
theorem Int.sub_self (a : Int) :
a - a = 0
@[simp]
theorem Int.sub_zero (a : Int) :
a - 0 = a
@[simp]
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 * = -(m * )
@[simp]
theorem Int.negSucc_mul_ofNat (m : Nat) (n : Nat) :
* n = -( * n)
@[simp]
theorem Int.negSucc_mul_negSucc (m : Nat) (n : Nat) :
= () * ()
theorem Int.mul_comm (a : Int) (b : Int) :
a * b = b * a
theorem Int.ofNat_mul_negOfNat (m : Nat) (n : Nat) :
m * = Int.negOfNat (m * n)
theorem Int.negOfNat_mul_ofNat (m : Nat) (n : Nat) :
* n = Int.negOfNat (m * n)
theorem Int.negSucc_mul_negOfNat (m : Nat) (n : Nat) :
= Int.ofNat ( * n)
theorem Int.negOfNat_mul_negSucc (m : Nat) (n : Nat) :
= Int.ofNat (n * )
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.ofNat_mul_subNatNat (m : Nat) (n : Nat) (k : Nat) :
m * = Int.subNatNat (m * n) (m * k)
theorem Int.negOfNat_add (m : Nat) (n : Nat) :
theorem Int.negSucc_mul_subNatNat (m : Nat) (n : Nat) (k : Nat) :
= Int.subNatNat ( * k) ( * 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
@[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) :
= -n - 1
theorem Int.subNatNat_eq_coe {m : Nat} {n : Nat} :
= 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) :
* () = a
@[simp]
theorem Int.sign_mul (a : Int) (b : Int) :
Int.sign (a * b) =

## Order properties of the integers #

theorem Int.nonneg_def {a : Int} :
∃ (n : Nat), a = n
theorem Int.NonNeg.elim {a : Int} :
∃ (n : Nat), a = n
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 = ()
theorem Int.lt_add_succ (a : Int) (n : Nat) :
a < a + ()
theorem Int.lt.intro {a : Int} {b : Int} {n : Nat} (h : a + () = b) :
a < b
theorem Int.lt.dest {a : Int} {b : Int} (h : a < b) :
∃ (n : Nat), a + () = 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 < ()
@[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.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 bb 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 = ()
theorem Int.le_natAbs {a : Int} :
a ()
theorem Int.negSucc_lt_zero (n : Nat) :
< 0
@[simp]
@[simp]
theorem Int.negSucc_not_pos (n : Nat) :
theorem Int.eq_negSucc_of_lt_zero {a : Int} :
a < 0∃ (n : Nat), a =
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 : Nat), a = -n
theorem Int.natAbs_of_nonneg {a : Int} (H : 0 a) :
() = a
theorem Int.ofNat_natAbs_of_nonpos {a : Int} (H : a 0) :
() = -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) :
= 1
theorem Int.sign_eq_neg_one_of_neg {a : Int} (h : a < 0) :
= -1
theorem Int.eq_zero_of_sign_eq_zero {a : Int} :
= 0a = 0
theorem Int.pos_of_sign_eq_one {a : Int} :
= 10 < a
theorem Int.neg_of_sign_eq_neg_one {a : Int} :
= -1a < 0
theorem Int.sign_eq_one_iff_pos (a : Int) :
= 1 0 < a
theorem Int.sign_eq_zero_iff_zero (a : Int) :
= 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.mul_eq_mul_left_iff {a : Int} {b : Int} {c : Int} (h : c 0) :
c * a = c * b a = b
theorem Int.mul_eq_mul_right_iff {a : Int} {b : Int} {c : Int} (h : c 0) :
a * c = b * c a = b
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() = a
theorem Int.eq_natAbs_iff_mul_eq_zero {a : Int} {n : Nat} :
= n (a - n) * (a + n) = 0
theorem Int.natAbs_add_le (a : Int) (b : Int) :
theorem Int.natAbs_sub_le (a : Int) (b : Int) :
theorem Int.negSucc_eq' (m : Nat) :
= -m - 1
theorem Int.natAbs_lt_natAbs_of_nonneg_of_lt {a : Int} {b : Int} (w₁ : 0 a) (w₂ : a < b) :

### toNat #

theorem Int.toNat_eq_max (a : Int) :
() = max a 0
@[simp]
theorem Int.toNat_zero :
= 0
@[simp]
theorem Int.toNat_one :
= 1
@[simp]
theorem Int.toNat_of_nonneg {a : Int} (h : 0 a) :
() = a
@[simp]
theorem Int.toNat_ofNat (n : Nat) :
= n
@[simp]
theorem Int.toNat_ofNat_add_one {n : Nat} :
Int.toNat (n + 1) = n + 1
theorem Int.self_le_toNat (a : Int) :
a ()
@[simp]
theorem Int.le_toNat {n : Nat} {z : Int} (h : 0 z) :
n n z
@[simp]
theorem Int.toNat_lt {n : Nat} {z : Int} (h : 0 z) :
< n z < n
theorem Int.toNat_add {a : Int} {b : Int} (ha : 0 a) (hb : 0 b) :
Int.toNat (a + b) =
theorem Int.toNat_add_nat {a : Int} (ha : 0 a) (n : Nat) :
Int.toNat (a + n) = + n
@[simp]
theorem Int.pred_toNat (i : Int) :
Int.toNat (i - 1) = - 1
@[simp]
theorem Int.toNat_sub_toNat_neg (n : Int) :
() - (Int.toNat (-n)) = n
theorem Int.mem_toNat' (a : Int) (n : Nat) :
= 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