mathlib documentation

core.init.data.int.order

def int.nonneg  :
→ Prop

Equations
def int.le  :
→ Prop

Equations
@[instance]

Equations
def int.lt  :
→ Prop

Equations
@[instance]

Equations

Equations
@[instance]
def int.decidable_le (a b : ) :

Equations
@[instance]
def int.decidable_lt (a b : ) :
decidable (a < b)

Equations
theorem int.lt_iff_add_one_le (a b : ) :
a < b a + 1 b

theorem int.nonneg.elim {a : } :
a.nonneg(∃ (n : ), a = n)

theorem int.le.intro_sub {a b : } {n : } :
b - a = na b

theorem int.le.intro {a b : } {n : } :
a + n = ba b

theorem int.le.dest_sub {a b : } :
a b(∃ (n : ), b - a = n)

theorem int.le.dest {a b : } :
a b(∃ (n : ), a + n = b)

theorem int.le.elim {a b : } (h : a b) {P : Prop} :
(∀ (n : ), a + n = b → P) → P

theorem int.le_total (a b : ) :
a b b a

theorem int.coe_nat_le_coe_nat_of_le {m n : } :
m nm n

theorem int.le_of_coe_nat_le_coe_nat {m n : } :
m nm n

theorem int.coe_nat_le_coe_nat_iff (m n : ) :
m n m n

theorem int.coe_zero_le (n : ) :
0 n

theorem int.eq_coe_of_zero_le {a : } :
0 a(∃ (n : ), a = n)

theorem int.eq_succ_of_zero_lt {a : } :
0 < a(∃ (n : ), a = (n.succ))

theorem int.lt_add_succ (a : ) (n : ) :
a < a + (n.succ)

theorem int.lt.intro {a b : } {n : } :
a + (n.succ) = ba < b

theorem int.lt.dest {a b : } :
a < b(∃ (n : ), a + (n.succ) = b)

theorem int.lt.elim {a b : } (h : a < b) {P : Prop} :
(∀ (n : ), a + (n.succ) = b → P) → P

theorem int.coe_nat_lt_coe_nat_iff (n m : ) :
n < m n < m

theorem int.lt_of_coe_nat_lt_coe_nat {m n : } :
m < nm < n

theorem int.coe_nat_lt_coe_nat_of_lt {m n : } :
m < nm < n

theorem int.le_refl (a : ) :
a a

theorem int.le_trans {a b c : } :
a bb ca c

theorem int.le_antisymm {a b : } :
a bb aa = b

theorem int.lt_irrefl (a : ) :
¬a < a

theorem int.ne_of_lt {a b : } :
a < ba b

theorem int.le_of_lt {a b : } :
a < ba b

theorem int.lt_iff_le_and_ne (a b : ) :
a < b a b a b

theorem int.lt_succ (a : ) :
a < a + 1

theorem int.add_le_add_left {a b : } (h : a b) (c : ) :
c + a c + b

theorem int.add_lt_add_left {a b : } (h : a < b) (c : ) :
c + a < c + b

theorem int.mul_nonneg {a b : } :
0 a0 b0 a * b

theorem int.mul_pos {a b : } :
0 < a0 < b0 < a * b

theorem int.zero_lt_one  :
0 < 1

theorem int.lt_iff_le_not_le {a b : } :
a < b a b ¬b a

theorem int.eq_nat_abs_of_zero_le {a : } :
0 aa = (a.nat_abs)

theorem int.le_nat_abs {a : } :

theorem int.neg_succ_lt_zero (n : ) :
-[1+ n] < 0

theorem int.eq_neg_succ_of_lt_zero {a : } :
a < 0(∃ (n : ), a = -[1+ n])

theorem int.eq_neg_of_eq_neg {a b : } :
a = -bb = -a

theorem int.neg_add_cancel_left (a b : ) :
-a + (a + b) = b

theorem int.add_neg_cancel_left (a b : ) :
a + (-a + b) = b

theorem int.add_neg_cancel_right (a b : ) :
a + b + -b = a

theorem int.neg_add_cancel_right (a b : ) :
a + -b + b = a

theorem int.sub_self (a : ) :
a - a = 0

theorem int.sub_eq_zero_of_eq {a b : } :
a = ba - b = 0

theorem int.eq_of_sub_eq_zero {a b : } :
a - b = 0a = b

theorem int.sub_eq_zero_iff_eq {a b : } :
a - b = 0 a = b

@[simp]
theorem int.neg_eq_of_add_eq_zero {a b : } :
a + b = 0-a = b

theorem int.neg_mul_eq_neg_mul (a b : ) :
-a * b = (-a) * b

theorem int.neg_mul_eq_mul_neg (a b : ) :
-a * b = a * -b

@[simp]
theorem int.neg_mul_eq_neg_mul_symm (a b : ) :
(-a) * b = -a * b

@[simp]
theorem int.mul_neg_eq_neg_mul_symm (a b : ) :
a * -b = -a * b

theorem int.neg_mul_neg (a b : ) :
(-a) * -b = a * b

theorem int.neg_mul_comm (a b : ) :
(-a) * b = a * -b

theorem int.mul_sub (a b c : ) :
a * (b - c) = a * b - a * c

theorem int.sub_mul (a b c : ) :
(a - b) * c = a * c - b * c

theorem int.le_of_add_le_add_left {a b c : } :
a + b a + cb c

theorem int.lt_of_add_lt_add_left {a b c : } :
a + b < a + cb < c

theorem int.add_le_add_right {a b : } (h : a b) (c : ) :
a + c b + c

theorem int.add_lt_add_right {a b : } (h : a < b) (c : ) :
a + c < b + c

theorem int.add_le_add {a b c d : } :
a bc da + c b + d

theorem int.le_add_of_nonneg_right {a b : } :
b 0a a + b

theorem int.le_add_of_nonneg_left {a b : } :
b 0a b + a

theorem int.add_lt_add {a b c d : } :
a < bc < da + c < b + d

theorem int.add_lt_add_of_le_of_lt {a b c d : } :
a bc < da + c < b + d

theorem int.add_lt_add_of_lt_of_le {a b c d : } :
a < bc da + c < b + d

theorem int.lt_add_of_pos_right (a : ) {b : } :
b > 0a < a + b

theorem int.lt_add_of_pos_left (a : ) {b : } :
b > 0a < b + a

theorem int.le_of_add_le_add_right {a b c : } :
a + b c + ba c

theorem int.lt_of_add_lt_add_right {a b c : } :
a + b < c + ba < c

theorem int.add_nonneg {a b : } :
0 a0 b0 a + b

theorem int.add_pos {a b : } :
0 < a0 < b0 < a + b

theorem int.add_pos_of_pos_of_nonneg {a b : } :
0 < a0 b0 < a + b

theorem int.add_pos_of_nonneg_of_pos {a b : } :
0 a0 < b0 < a + b

theorem int.add_nonpos {a b : } :
a 0b 0a + b 0

theorem int.add_neg {a b : } :
a < 0b < 0a + b < 0

theorem int.add_neg_of_neg_of_nonpos {a b : } :
a < 0b 0a + b < 0

theorem int.add_neg_of_nonpos_of_neg {a b : } :
a 0b < 0a + b < 0

theorem int.lt_add_of_le_of_pos {a b c : } :
b c0 < ab < c + a

theorem int.sub_add_cancel (a b : ) :
a - b + b = a

theorem int.add_sub_cancel (a b : ) :
a + b - b = a

theorem int.add_sub_assoc (a b c : ) :
a + b - c = a + (b - c)

theorem int.neg_le_neg {a b : } :
a b-b -a

theorem int.le_of_neg_le_neg {a b : } :
-b -aa b

theorem int.nonneg_of_neg_nonpos {a : } :
-a 00 a

theorem int.neg_nonpos_of_nonneg {a : } :
0 a-a 0

theorem int.nonpos_of_neg_nonneg {a : } :
0 -aa 0

theorem int.neg_nonneg_of_nonpos {a : } :
a 00 -a

theorem int.neg_lt_neg {a b : } :
a < b-b < -a

theorem int.lt_of_neg_lt_neg {a b : } :
-b < -aa < b

theorem int.pos_of_neg_neg {a : } :
-a < 00 < a

theorem int.neg_neg_of_pos {a : } :
0 < a-a < 0

theorem int.neg_of_neg_pos {a : } :
0 < -aa < 0

theorem int.neg_pos_of_neg {a : } :
a < 00 < -a

theorem int.le_neg_of_le_neg {a b : } :
a -bb -a

theorem int.neg_le_of_neg_le {a b : } :
-a b-b a

theorem int.lt_neg_of_lt_neg {a b : } :
a < -bb < -a

theorem int.neg_lt_of_neg_lt {a b : } :
-a < b-b < a

theorem int.sub_nonneg_of_le {a b : } :
b a0 a - b

theorem int.le_of_sub_nonneg {a b : } :
0 a - bb a

theorem int.sub_nonpos_of_le {a b : } :
a ba - b 0

theorem int.le_of_sub_nonpos {a b : } :
a - b 0a b

theorem int.sub_pos_of_lt {a b : } :
b < a0 < a - b

theorem int.lt_of_sub_pos {a b : } :
0 < a - bb < a

theorem int.sub_neg_of_lt {a b : } :
a < ba - b < 0

theorem int.lt_of_sub_neg {a b : } :
a - b < 0a < b

theorem int.add_le_of_le_neg_add {a b c : } :
b -a + ca + b c

theorem int.le_neg_add_of_add_le {a b c : } :
a + b cb -a + c

theorem int.add_le_of_le_sub_left {a b c : } :
b c - aa + b c

theorem int.le_sub_left_of_add_le {a b c : } :
a + b cb c - a

theorem int.add_le_of_le_sub_right {a b c : } :
a c - ba + b c

theorem int.le_sub_right_of_add_le {a b c : } :
a + b ca c - b

theorem int.le_add_of_neg_add_le {a b c : } :
-b + a ca b + c

theorem int.neg_add_le_of_le_add {a b c : } :
a b + c-b + a c

theorem int.le_add_of_sub_left_le {a b c : } :
a - b ca b + c

theorem int.sub_left_le_of_le_add {a b c : } :
a b + ca - b c

theorem int.le_add_of_sub_right_le {a b c : } :
a - c ba b + c

theorem int.sub_right_le_of_le_add {a b c : } :
a b + ca - c b

theorem int.le_add_of_neg_add_le_left {a b c : } :
-b + a ca b + c

theorem int.neg_add_le_left_of_le_add {a b c : } :
a b + c-b + a c

theorem int.le_add_of_neg_add_le_right {a b c : } :
-c + a ba b + c

theorem int.neg_add_le_right_of_le_add {a b c : } :
a b + c-c + a b

theorem int.le_add_of_neg_le_sub_left {a b c : } :
-a b - cc a + b

theorem int.neg_le_sub_left_of_le_add {a b c : } :
c a + b-a b - c

theorem int.le_add_of_neg_le_sub_right {a b c : } :
-b a - cc a + b

theorem int.neg_le_sub_right_of_le_add {a b c : } :
c a + b-b a - c

theorem int.sub_le_of_sub_le {a b c : } :
a - b ca - c b

theorem int.sub_le_sub_left {a b : } (h : a b) (c : ) :
c - b c - a

theorem int.sub_le_sub_right {a b : } (h : a b) (c : ) :
a - c b - c

theorem int.sub_le_sub {a b c d : } :
a bc da - d b - c

theorem int.add_lt_of_lt_neg_add {a b c : } :
b < -a + ca + b < c

theorem int.lt_neg_add_of_add_lt {a b c : } :
a + b < cb < -a + c

theorem int.add_lt_of_lt_sub_left {a b c : } :
b < c - aa + b < c

theorem int.lt_sub_left_of_add_lt {a b c : } :
a + b < cb < c - a

theorem int.add_lt_of_lt_sub_right {a b c : } :
a < c - ba + b < c

theorem int.lt_sub_right_of_add_lt {a b c : } :
a + b < ca < c - b

theorem int.lt_add_of_neg_add_lt {a b c : } :
-b + a < ca < b + c

theorem int.neg_add_lt_of_lt_add {a b c : } :
a < b + c-b + a < c

theorem int.lt_add_of_sub_left_lt {a b c : } :
a - b < ca < b + c

theorem int.sub_left_lt_of_lt_add {a b c : } :
a < b + ca - b < c

theorem int.lt_add_of_sub_right_lt {a b c : } :
a - c < ba < b + c

theorem int.sub_right_lt_of_lt_add {a b c : } :
a < b + ca - c < b

theorem int.lt_add_of_neg_add_lt_left {a b c : } :
-b + a < ca < b + c

theorem int.neg_add_lt_left_of_lt_add {a b c : } :
a < b + c-b + a < c

theorem int.lt_add_of_neg_add_lt_right {a b c : } :
-c + a < ba < b + c

theorem int.neg_add_lt_right_of_lt_add {a b c : } :
a < b + c-c + a < b

theorem int.lt_add_of_neg_lt_sub_left {a b c : } :
-a < b - cc < a + b

theorem int.neg_lt_sub_left_of_lt_add {a b c : } :
c < a + b-a < b - c

theorem int.lt_add_of_neg_lt_sub_right {a b c : } :
-b < a - cc < a + b

theorem int.neg_lt_sub_right_of_lt_add {a b c : } :
c < a + b-b < a - c

theorem int.sub_lt_of_sub_lt {a b c : } :
a - b < ca - c < b

theorem int.sub_lt_sub_left {a b : } (h : a < b) (c : ) :
c - b < c - a

theorem int.sub_lt_sub_right {a b : } (h : a < b) (c : ) :
a - c < b - c

theorem int.sub_lt_sub {a b c d : } :
a < bc < da - d < b - c

theorem int.sub_lt_sub_of_le_of_lt {a b c d : } :
a bc < da - d < b - c

theorem int.sub_lt_sub_of_lt_of_le {a b c d : } :
a < bc da - d < b - c

theorem int.sub_le_self (a : ) {b : } :
b 0a - b a

theorem int.sub_lt_self (a : ) {b : } :
b > 0a - b < a

theorem int.add_le_add_three {a b c d e f : } :
a db ec fa + b + c d + e + f

theorem int.mul_lt_mul_of_pos_left {a b c : } :
a < b0 < cc * a < c * b

theorem int.mul_lt_mul_of_pos_right {a b c : } :
a < b0 < ca * c < b * c

theorem int.mul_le_mul_of_nonneg_left {a b c : } :
a b0 cc * a c * b

theorem int.mul_le_mul_of_nonneg_right {a b c : } :
a b0 ca * c b * c

theorem int.mul_le_mul {a b c d : } :
a cb d0 b0 ca * b c * d

theorem int.mul_nonpos_of_nonneg_of_nonpos {a b : } :
a 0b 0a * b 0

theorem int.mul_nonpos_of_nonpos_of_nonneg {a b : } :
a 0b 0a * b 0

theorem int.mul_lt_mul {a b c d : } :
a < cb d0 < b0 ca * b < c * d

theorem int.mul_lt_mul' {a b c d : } :
a cb < db 0c > 0a * b < c * d

theorem int.mul_neg_of_pos_of_neg {a b : } :
a > 0b < 0a * b < 0

theorem int.mul_neg_of_neg_of_pos {a b : } :
a < 0b > 0a * b < 0

theorem int.mul_le_mul_of_nonpos_right {a b c : } :
b ac 0a * c b * c

theorem int.mul_nonneg_of_nonpos_of_nonpos {a b : } :
a 0b 00 a * b

theorem int.mul_lt_mul_of_neg_left {a b c : } :
b < ac < 0c * a < c * b

theorem int.mul_lt_mul_of_neg_right {a b c : } :
b < ac < 0a * c < b * c

theorem int.mul_pos_of_neg_of_neg {a b : } :
a < 0b < 00 < a * b

theorem int.mul_self_le_mul_self {a b : } :
0 aa ba * a b * b

theorem int.mul_self_lt_mul_self {a b : } :
0 aa < ba * a < b * b

theorem int.of_nat_nonneg (n : ) :

theorem int.coe_succ_pos (n : ) :
(n.succ) > 0

theorem int.exists_eq_neg_of_nat {a : } :
a 0(∃ (n : ), a = -n)

theorem int.nat_abs_of_nonneg {a : } :
a 0(a.nat_abs) = a

theorem int.of_nat_nat_abs_of_nonpos {a : } :
a 0(a.nat_abs) = -a

theorem int.lt_of_add_one_le {a b : } :
a + 1 ba < b

theorem int.add_one_le_of_lt {a b : } :
a < ba + 1 b

theorem int.lt_add_one_of_le {a b : } :
a ba < b + 1

theorem int.le_of_lt_add_one {a b : } :
a < b + 1a b

theorem int.sub_one_le_of_lt {a b : } :
a ba - 1 < b

theorem int.lt_of_sub_one_le {a b : } :
a - 1 < ba b

theorem int.le_sub_one_of_lt {a b : } :
a < ba b - 1

theorem int.lt_of_le_sub_one {a b : } :
a b - 1a < b

theorem int.sign_of_succ (n : ) :
(n.succ).sign = 1

theorem int.sign_eq_one_of_pos {a : } :
0 < aa.sign = 1

theorem int.sign_eq_neg_one_of_neg {a : } :
a < 0a.sign = -1

theorem int.eq_zero_of_sign_eq_zero {a : } :
a.sign = 0a = 0

theorem int.pos_of_sign_eq_one {a : } :
a.sign = 10 < a

theorem int.neg_of_sign_eq_neg_one {a : } :
a.sign = -1a < 0

theorem int.sign_eq_one_iff_pos (a : ) :
a.sign = 1 0 < a

theorem int.sign_eq_neg_one_iff_neg (a : ) :
a.sign = -1 a < 0

theorem int.sign_eq_zero_iff_zero (a : ) :
a.sign = 0 a = 0

theorem int.eq_zero_or_eq_zero_of_mul_eq_zero {a b : } :
a * b = 0a = 0 b = 0

theorem int.eq_of_mul_eq_mul_right {a b c : } :
a 0b * a = c * ab = c

theorem int.eq_of_mul_eq_mul_left {a b c : } :
a 0a * b = a * cb = c

theorem int.eq_one_of_mul_eq_self_left {a b : } :
a 0b * a = ab = 1

theorem int.eq_one_of_mul_eq_self_right {a b : } :
b 0b * a = ba = 1