mathlib3 documentation

core / init.data.int.order

@[irreducible]
def int.nonneg (a : ) :
Prop
Equations
@[protected]
def int.le (a b : ) :
Prop
Equations
@[protected, instance]
Equations
@[protected]
def int.lt (a b : ) :
Prop
Equations
@[protected, instance]
Equations
Equations
@[protected, instance]
def int.decidable_le (a b : ) :
Equations
@[protected, 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 : } (h : b - a = n) :
a b
theorem int.le.intro {a b : } {n : } (h : a + n = b) :
a b
theorem int.le.dest_sub {a b : } (h : a b) :
(n : ), b - a = n
theorem int.le.dest {a b : } (h : a b) :
(n : ), a + n = b
theorem int.le.elim {a b : } (h : a b) {P : Prop} (h' : (n : ), a + n = b P) :
P
@[protected]
theorem int.le_total (a b : ) :
a b b a
theorem int.coe_nat_le_coe_nat_of_le {m n : } (h : m n) :
theorem int.le_of_coe_nat_le_coe_nat {m n : } (h : m n) :
m 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 : } (h : 0 a) :
(n : ), a = n
theorem int.eq_succ_of_zero_lt {a : } (h : 0 < a) :
(n : ), a = (n.succ)
theorem int.lt_add_succ (a : ) (n : ) :
a < a + (n.succ)
theorem int.lt.intro {a b : } {n : } (h : a + (n.succ) = b) :
a < b
theorem int.lt.dest {a b : } (h : a < b) :
(n : ), a + (n.succ) = b
theorem int.lt.elim {a b : } (h : a < b) {P : Prop} (h' : (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 : } (h : m < n) :
m < n
theorem int.coe_nat_lt_coe_nat_of_lt {m n : } (h : m < n) :

show that the integers form an ordered additive group

@[protected]
theorem int.le_refl (a : ) :
a a
@[protected]
theorem int.le_trans {a b c : } (h₁ : a b) (h₂ : b c) :
a c
@[protected]
theorem int.le_antisymm {a b : } (h₁ : a b) (h₂ : b a) :
a = b
@[protected]
theorem int.lt_irrefl (a : ) :
¬a < a
@[protected]
theorem int.ne_of_lt {a b : } (h : a < b) :
a b
theorem int.le_of_lt {a b : } (h : a < b) :
a b
@[protected]
theorem int.lt_iff_le_and_ne (a b : ) :
a < b a b a b
theorem int.lt_succ (a : ) :
a < a + 1
@[protected]
theorem int.add_le_add_left {a b : } (h : a b) (c : ) :
c + a c + b
@[protected]
theorem int.add_lt_add_left {a b : } (h : a < b) (c : ) :
c + a < c + b
@[protected]
theorem int.mul_nonneg {a b : } (ha : 0 a) (hb : 0 b) :
0 a * b
@[protected]
theorem int.mul_pos {a b : } (ha : 0 < a) (hb : 0 < b) :
0 < a * b
@[protected]
theorem int.zero_lt_one  :
0 < 1
@[protected]
theorem int.lt_iff_le_not_le {a b : } :
a < b a b ¬b a
theorem int.eq_nat_abs_of_zero_le {a : } (h : 0 a) :
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])

int is an ordered add comm group

@[protected]
theorem int.eq_neg_of_eq_neg {a b : } (h : a = -b) :
b = -a
@[protected]
theorem int.neg_add_cancel_left (a b : ) :
-a + (a + b) = b
@[protected]
theorem int.add_neg_cancel_left (a b : ) :
a + (-a + b) = b
@[protected]
theorem int.add_neg_cancel_right (a b : ) :
a + b + -b = a
@[protected]
theorem int.neg_add_cancel_right (a b : ) :
a + -b + b = a
@[protected]
theorem int.sub_self (a : ) :
a - a = 0
@[protected]
theorem int.sub_eq_zero_of_eq {a b : } (h : a = b) :
a - b = 0
@[protected]
theorem int.eq_of_sub_eq_zero {a b : } (h : a - b = 0) :
a = b
@[protected]
theorem int.sub_eq_zero_iff_eq {a b : } :
a - b = 0 a = b
@[protected, simp]
theorem int.neg_eq_of_add_eq_zero {a b : } (h : a + b = 0) :
-a = b
@[protected]
theorem int.neg_mul_eq_neg_mul (a b : ) :
-(a * b) = -a * b
@[protected]
theorem int.neg_mul_eq_mul_neg (a b : ) :
-(a * b) = a * -b
theorem int.neg_mul_eq_neg_mul_symm (a b : ) :
-a * b = -(a * b)
theorem int.mul_neg_eq_neg_mul_symm (a b : ) :
a * -b = -(a * b)
@[protected]
theorem int.neg_mul_neg (a b : ) :
-a * -b = a * b
@[protected]
theorem int.neg_mul_comm (a b : ) :
-a * b = a * -b
@[protected]
theorem int.mul_sub (a b c : ) :
a * (b - c) = a * b - a * c
@[protected]
theorem int.sub_mul (a b c : ) :
(a - b) * c = a * c - b * c
@[protected]
theorem int.le_of_add_le_add_left {a b c : } (h : a + b a + c) :
b c
@[protected]
theorem int.lt_of_add_lt_add_left {a b c : } (h : a + b < a + c) :
b < c
@[protected]
theorem int.add_le_add_right {a b : } (h : a b) (c : ) :
a + c b + c
@[protected]
theorem int.add_lt_add_right {a b : } (h : a < b) (c : ) :
a + c < b + c
@[protected]
theorem int.add_le_add {a b c d : } (h₁ : a b) (h₂ : c d) :
a + c b + d
@[protected]
theorem int.le_add_of_nonneg_right {a b : } (h : 0 b) :
a a + b
@[protected]
theorem int.le_add_of_nonneg_left {a b : } (h : 0 b) :
a b + a
@[protected]
theorem int.add_lt_add {a b c d : } (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
@[protected]
theorem int.add_lt_add_of_le_of_lt {a b c d : } (h₁ : a b) (h₂ : c < d) :
a + c < b + d
@[protected]
theorem int.add_lt_add_of_lt_of_le {a b c d : } (h₁ : a < b) (h₂ : c d) :
a + c < b + d
@[protected]
theorem int.lt_add_of_pos_right (a : ) {b : } (h : 0 < b) :
a < a + b
@[protected]
theorem int.lt_add_of_pos_left (a : ) {b : } (h : 0 < b) :
a < b + a
@[protected]
theorem int.le_of_add_le_add_right {a b c : } (h : a + b c + b) :
a c
@[protected]
theorem int.lt_of_add_lt_add_right {a b c : } (h : a + b < c + b) :
a < c
@[protected]
theorem int.add_nonneg {a b : } (ha : 0 a) (hb : 0 b) :
0 a + b
@[protected]
theorem int.add_pos {a b : } (ha : 0 < a) (hb : 0 < b) :
0 < a + b
@[protected]
theorem int.add_pos_of_pos_of_nonneg {a b : } (ha : 0 < a) (hb : 0 b) :
0 < a + b
@[protected]
theorem int.add_pos_of_nonneg_of_pos {a b : } (ha : 0 a) (hb : 0 < b) :
0 < a + b
@[protected]
theorem int.add_nonpos {a b : } (ha : a 0) (hb : b 0) :
a + b 0
@[protected]
theorem int.add_neg {a b : } (ha : a < 0) (hb : b < 0) :
a + b < 0
@[protected]
theorem int.add_neg_of_neg_of_nonpos {a b : } (ha : a < 0) (hb : b 0) :
a + b < 0
@[protected]
theorem int.add_neg_of_nonpos_of_neg {a b : } (ha : a 0) (hb : b < 0) :
a + b < 0
@[protected]
theorem int.lt_add_of_le_of_pos {a b c : } (hbc : b c) (ha : 0 < a) :
b < c + a
@[protected]
theorem int.sub_add_cancel (a b : ) :
a - b + b = a
@[protected]
theorem int.add_sub_cancel (a b : ) :
a + b - b = a
@[protected]
theorem int.add_sub_assoc (a b c : ) :
a + b - c = a + (b - c)
@[protected]
theorem int.neg_le_neg {a b : } (h : a b) :
-b -a
@[protected]
theorem int.le_of_neg_le_neg {a b : } (h : -b -a) :
a b
@[protected]
theorem int.nonneg_of_neg_nonpos {a : } (h : -a 0) :
0 a
@[protected]
theorem int.neg_nonpos_of_nonneg {a : } (h : 0 a) :
-a 0
@[protected]
theorem int.nonpos_of_neg_nonneg {a : } (h : 0 -a) :
a 0
@[protected]
theorem int.neg_nonneg_of_nonpos {a : } (h : a 0) :
0 -a
@[protected]
theorem int.neg_lt_neg {a b : } (h : a < b) :
-b < -a
@[protected]
theorem int.lt_of_neg_lt_neg {a b : } (h : -b < -a) :
a < b
@[protected]
theorem int.pos_of_neg_neg {a : } (h : -a < 0) :
0 < a
@[protected]
theorem int.neg_neg_of_pos {a : } (h : 0 < a) :
-a < 0
@[protected]
theorem int.neg_of_neg_pos {a : } (h : 0 < -a) :
a < 0
@[protected]
theorem int.neg_pos_of_neg {a : } (h : a < 0) :
0 < -a
@[protected]
theorem int.le_neg_of_le_neg {a b : } (h : a -b) :
b -a
@[protected]
theorem int.neg_le_of_neg_le {a b : } (h : -a b) :
-b a
@[protected]
theorem int.lt_neg_of_lt_neg {a b : } (h : a < -b) :
b < -a
@[protected]
theorem int.neg_lt_of_neg_lt {a b : } (h : -a < b) :
-b < a
@[protected]
theorem int.sub_nonneg_of_le {a b : } (h : b a) :
0 a - b
@[protected]
theorem int.le_of_sub_nonneg {a b : } (h : 0 a - b) :
b a
@[protected]
theorem int.sub_nonpos_of_le {a b : } (h : a b) :
a - b 0
@[protected]
theorem int.le_of_sub_nonpos {a b : } (h : a - b 0) :
a b
@[protected]
theorem int.sub_pos_of_lt {a b : } (h : b < a) :
0 < a - b
@[protected]
theorem int.lt_of_sub_pos {a b : } (h : 0 < a - b) :
b < a
@[protected]
theorem int.sub_neg_of_lt {a b : } (h : a < b) :
a - b < 0
@[protected]
theorem int.lt_of_sub_neg {a b : } (h : a - b < 0) :
a < b
@[protected]
theorem int.add_le_of_le_neg_add {a b c : } (h : b -a + c) :
a + b c
@[protected]
theorem int.le_neg_add_of_add_le {a b c : } (h : a + b c) :
b -a + c
@[protected]
theorem int.add_le_of_le_sub_left {a b c : } (h : b c - a) :
a + b c
@[protected]
theorem int.le_sub_left_of_add_le {a b c : } (h : a + b c) :
b c - a
@[protected]
theorem int.add_le_of_le_sub_right {a b c : } (h : a c - b) :
a + b c
@[protected]
theorem int.le_sub_right_of_add_le {a b c : } (h : a + b c) :
a c - b
@[protected]
theorem int.le_add_of_neg_add_le {a b c : } (h : -b + a c) :
a b + c
@[protected]
theorem int.neg_add_le_of_le_add {a b c : } (h : a b + c) :
-b + a c
@[protected]
theorem int.le_add_of_sub_left_le {a b c : } (h : a - b c) :
a b + c
@[protected]
theorem int.sub_left_le_of_le_add {a b c : } (h : a b + c) :
a - b c
@[protected]
theorem int.le_add_of_sub_right_le {a b c : } (h : a - c b) :
a b + c
@[protected]
theorem int.sub_right_le_of_le_add {a b c : } (h : a b + c) :
a - c b
@[protected]
theorem int.le_add_of_neg_add_le_left {a b c : } (h : -b + a c) :
a b + c
@[protected]
theorem int.neg_add_le_left_of_le_add {a b c : } (h : a b + c) :
-b + a c
@[protected]
theorem int.le_add_of_neg_add_le_right {a b c : } (h : -c + a b) :
a b + c
@[protected]
theorem int.neg_add_le_right_of_le_add {a b c : } (h : a b + c) :
-c + a b
@[protected]
theorem int.le_add_of_neg_le_sub_left {a b c : } (h : -a b - c) :
c a + b
@[protected]
theorem int.neg_le_sub_left_of_le_add {a b c : } (h : c a + b) :
-a b - c
@[protected]
theorem int.le_add_of_neg_le_sub_right {a b c : } (h : -b a - c) :
c a + b
@[protected]
theorem int.neg_le_sub_right_of_le_add {a b c : } (h : c a + b) :
-b a - c
@[protected]
theorem int.sub_le_of_sub_le {a b c : } (h : a - b c) :
a - c b
@[protected]
theorem int.sub_le_sub_left {a b : } (h : a b) (c : ) :
c - b c - a
@[protected]
theorem int.sub_le_sub_right {a b : } (h : a b) (c : ) :
a - c b - c
@[protected]
theorem int.sub_le_sub {a b c d : } (hab : a b) (hcd : c d) :
a - d b - c
@[protected]
theorem int.add_lt_of_lt_neg_add {a b c : } (h : b < -a + c) :
a + b < c
@[protected]
theorem int.lt_neg_add_of_add_lt {a b c : } (h : a + b < c) :
b < -a + c
@[protected]
theorem int.add_lt_of_lt_sub_left {a b c : } (h : b < c - a) :
a + b < c
@[protected]
theorem int.lt_sub_left_of_add_lt {a b c : } (h : a + b < c) :
b < c - a
@[protected]
theorem int.add_lt_of_lt_sub_right {a b c : } (h : a < c - b) :
a + b < c
@[protected]
theorem int.lt_sub_right_of_add_lt {a b c : } (h : a + b < c) :
a < c - b
@[protected]
theorem int.lt_add_of_neg_add_lt {a b c : } (h : -b + a < c) :
a < b + c
@[protected]
theorem int.neg_add_lt_of_lt_add {a b c : } (h : a < b + c) :
-b + a < c
@[protected]
theorem int.lt_add_of_sub_left_lt {a b c : } (h : a - b < c) :
a < b + c
@[protected]
theorem int.sub_left_lt_of_lt_add {a b c : } (h : a < b + c) :
a - b < c
@[protected]
theorem int.lt_add_of_sub_right_lt {a b c : } (h : a - c < b) :
a < b + c
@[protected]
theorem int.sub_right_lt_of_lt_add {a b c : } (h : a < b + c) :
a - c < b
@[protected]
theorem int.lt_add_of_neg_add_lt_left {a b c : } (h : -b + a < c) :
a < b + c
@[protected]
theorem int.neg_add_lt_left_of_lt_add {a b c : } (h : a < b + c) :
-b + a < c
@[protected]
theorem int.lt_add_of_neg_add_lt_right {a b c : } (h : -c + a < b) :
a < b + c
@[protected]
theorem int.neg_add_lt_right_of_lt_add {a b c : } (h : a < b + c) :
-c + a < b
@[protected]
theorem int.lt_add_of_neg_lt_sub_left {a b c : } (h : -a < b - c) :
c < a + b
@[protected]
theorem int.neg_lt_sub_left_of_lt_add {a b c : } (h : c < a + b) :
-a < b - c
@[protected]
theorem int.lt_add_of_neg_lt_sub_right {a b c : } (h : -b < a - c) :
c < a + b
@[protected]
theorem int.neg_lt_sub_right_of_lt_add {a b c : } (h : c < a + b) :
-b < a - c
@[protected]
theorem int.sub_lt_of_sub_lt {a b c : } (h : a - b < c) :
a - c < b
@[protected]
theorem int.sub_lt_sub_left {a b : } (h : a < b) (c : ) :
c - b < c - a
@[protected]
theorem int.sub_lt_sub_right {a b : } (h : a < b) (c : ) :
a - c < b - c
@[protected]
theorem int.sub_lt_sub {a b c d : } (hab : a < b) (hcd : c < d) :
a - d < b - c
@[protected]
theorem int.sub_lt_sub_of_le_of_lt {a b c d : } (hab : a b) (hcd : c < d) :
a - d < b - c
@[protected]
theorem int.sub_lt_sub_of_lt_of_le {a b c d : } (hab : a < b) (hcd : c d) :
a - d < b - c
@[protected]
theorem int.sub_le_self (a : ) {b : } (h : 0 b) :
a - b a
@[protected]
theorem int.sub_lt_self (a : ) {b : } (h : 0 < b) :
a - b < a
@[protected]
theorem int.add_le_add_three {a b c d e f : } (h₁ : a d) (h₂ : b e) (h₃ : c f) :
a + b + c d + e + f

missing facts

@[protected]
theorem int.mul_lt_mul_of_pos_left {a b c : } (h₁ : a < b) (h₂ : 0 < c) :
c * a < c * b
@[protected]
theorem int.mul_lt_mul_of_pos_right {a b c : } (h₁ : a < b) (h₂ : 0 < c) :
a * c < b * c
@[protected]
theorem int.mul_le_mul_of_nonneg_left {a b c : } (h₁ : a b) (h₂ : 0 c) :
c * a c * b
@[protected]
theorem int.mul_le_mul_of_nonneg_right {a b c : } (h₁ : a b) (h₂ : 0 c) :
a * c b * c
@[protected]
theorem int.mul_le_mul {a b c d : } (hac : a c) (hbd : b d) (nn_b : 0 b) (nn_c : 0 c) :
a * b c * d
@[protected]
theorem int.mul_nonpos_of_nonneg_of_nonpos {a b : } (ha : 0 a) (hb : b 0) :
a * b 0
@[protected]
theorem int.mul_nonpos_of_nonpos_of_nonneg {a b : } (ha : a 0) (hb : 0 b) :
a * b 0
@[protected]
theorem int.mul_lt_mul {a b c d : } (hac : a < c) (hbd : b d) (pos_b : 0 < b) (nn_c : 0 c) :
a * b < c * d
@[protected]
theorem int.mul_lt_mul' {a b c d : } (h1 : a c) (h2 : b < d) (h3 : 0 b) (h4 : 0 < c) :
a * b < c * d
@[protected]
theorem int.mul_neg_of_pos_of_neg {a b : } (ha : 0 < a) (hb : b < 0) :
a * b < 0
@[protected]
theorem int.mul_neg_of_neg_of_pos {a b : } (ha : a < 0) (hb : 0 < b) :
a * b < 0
@[protected]
theorem int.mul_le_mul_of_nonpos_right {a b c : } (h : b a) (hc : c 0) :
a * c b * c
@[protected]
theorem int.mul_nonneg_of_nonpos_of_nonpos {a b : } (ha : a 0) (hb : b 0) :
0 a * b
@[protected]
theorem int.mul_lt_mul_of_neg_left {a b c : } (h : b < a) (hc : c < 0) :
c * a < c * b
@[protected]
theorem int.mul_lt_mul_of_neg_right {a b c : } (h : b < a) (hc : c < 0) :
a * c < b * c
@[protected]
theorem int.mul_pos_of_neg_of_neg {a b : } (ha : a < 0) (hb : b < 0) :
0 < a * b
@[protected]
theorem int.mul_self_le_mul_self {a b : } (h1 : 0 a) (h2 : a b) :
a * a b * b
@[protected]
theorem int.mul_self_lt_mul_self {a b : } (h1 : 0 a) (h2 : a < b) :
a * a < b * b

more facts specific to int

theorem int.of_nat_nonneg (n : ) :
theorem int.coe_succ_pos (n : ) :
0 < (n.succ)
theorem int.exists_eq_neg_of_nat {a : } (H : a 0) :
(n : ), a = -n
theorem int.nat_abs_of_nonneg {a : } (H : 0 a) :
theorem int.of_nat_nat_abs_of_nonpos {a : } (H : a 0) :
theorem int.lt_of_add_one_le {a b : } (H : a + 1 b) :
a < b
theorem int.add_one_le_of_lt {a b : } (H : a < b) :
a + 1 b
theorem int.lt_add_one_of_le {a b : } (H : a b) :
a < b + 1
theorem int.le_of_lt_add_one {a b : } (H : a < b + 1) :
a b
theorem int.sub_one_lt_of_le {a b : } (H : a b) :
a - 1 < b
theorem int.le_of_sub_one_lt {a b : } (H : a - 1 < b) :
a b
theorem int.le_sub_one_of_lt {a b : } (H : a < b) :
a b - 1
theorem int.lt_of_le_sub_one {a b : } (H : a b - 1) :
a < b
theorem int.sign_of_succ (n : ) :
(n.succ).sign = 1
theorem int.sign_eq_one_of_pos {a : } (h : 0 < a) :
a.sign = 1
theorem int.sign_eq_neg_one_of_neg {a : } (h : a < 0) :
a.sign = -1
theorem int.eq_zero_of_sign_eq_zero {a : } :
a.sign = 0 a = 0
theorem int.pos_of_sign_eq_one {a : } :
a.sign = 1 0 < a
theorem int.neg_of_sign_eq_neg_one {a : } :
a.sign = -1 a < 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
@[protected]
theorem int.eq_zero_or_eq_zero_of_mul_eq_zero {a b : } (h : a * b = 0) :
a = 0 b = 0
@[protected]
theorem int.eq_of_mul_eq_mul_right {a b c : } (ha : a 0) (h : b * a = c * a) :
b = c
@[protected]
theorem int.eq_of_mul_eq_mul_left {a b c : } (ha : a 0) (h : a * b = a * c) :
b = c
theorem int.eq_one_of_mul_eq_self_left {a b : } (Hpos : a 0) (H : b * a = a) :
b = 1
theorem int.eq_one_of_mul_eq_self_right {a b : } (Hpos : b 0) (H : b * a = b) :
a = 1