HepLean Documentation
Init
.
Data
.
Int
.
Order
Search
Google site search
return to top
source
Imports
Init.ByCases
Init.Data.Int.Lemmas
Imported by
Int
.
nonneg_def
Int
.
NonNeg
.
elim
Int
.
nonneg_or_nonneg_neg
Int
.
le_def
Int
.
lt_iff_add_one_le
Int
.
le
.
intro_sub
Int
.
le
.
intro
Int
.
le
.
dest_sub
Int
.
le
.
dest
Int
.
le_total
Int
.
ofNat_le
Int
.
ofNat_zero_le
Int
.
eq_ofNat_of_zero_le
Int
.
eq_succ_of_zero_lt
Int
.
lt_add_succ
Int
.
lt
.
intro
Int
.
lt
.
dest
Int
.
ofNat_lt
Int
.
ofNat_pos
Int
.
ofNat_nonneg
Int
.
ofNat_succ_pos
Int
.
le_refl
Int
.
le_trans
Int
.
le_antisymm
Int
.
lt_irrefl
Int
.
ne_of_lt
Int
.
ne_of_gt
Int
.
le_of_lt
Int
.
lt_iff_le_and_ne
Int
.
lt_succ
Int
.
zero_lt_one
Int
.
lt_iff_le_not_le
Int
.
lt_of_not_ge
Int
.
not_le_of_gt
Int
.
not_le
Int
.
not_lt
Int
.
lt_trichotomy
Int
.
ne_iff_lt_or_gt
Int
.
lt_or_gt_of_ne
Int
.
eq_iff_le_and_ge
Int
.
lt_of_le_of_lt
Int
.
lt_of_lt_of_le
Int
.
lt_trans
Int
.
instTransLe
Int
.
instTransLtLe
Int
.
instTransLeLt
Int
.
instTransLt
Int
.
min_def
Int
.
max_def
Int
.
min_comm
Int
.
instCommutativeMin
Int
.
min_le_right
Int
.
min_le_left
Int
.
min_eq_left
Int
.
min_eq_right
Int
.
le_min
Int
.
max_comm
Int
.
instCommutativeMax
Int
.
le_max_left
Int
.
le_max_right
Int
.
max_le
Int
.
max_eq_right
Int
.
max_eq_left
Int
.
eq_natAbs_of_zero_le
Int
.
le_natAbs
Int
.
negSucc_lt_zero
Int
.
negSucc_le_zero
Int
.
negSucc_not_nonneg
Int
.
ofNat_max_zero
Int
.
zero_max_ofNat
Int
.
negSucc_max_zero
Int
.
zero_max_negSucc
Int
.
add_le_add_left
Int
.
add_lt_add_left
Int
.
add_le_add_right
Int
.
add_lt_add_right
Int
.
le_of_add_le_add_left
Int
.
le_of_add_le_add_right
Int
.
add_le_add_iff_left
Int
.
add_le_add_iff_right
Int
.
add_le_add
Int
.
le_add_of_nonneg_right
Int
.
le_add_of_nonneg_left
Int
.
neg_le_neg
Int
.
le_of_neg_le_neg
Int
.
neg_nonpos_of_nonneg
Int
.
neg_nonneg_of_nonpos
Int
.
neg_lt_neg
Int
.
neg_neg_of_pos
Int
.
neg_pos_of_neg
Int
.
sub_nonneg_of_le
Int
.
le_of_sub_nonneg
Int
.
sub_pos_of_lt
Int
.
lt_of_sub_pos
Int
.
sub_left_le_of_le_add
Int
.
sub_le_self
Int
.
sub_lt_self
Int
.
add_one_le_of_lt
Int
.
mul_nonneg
Int
.
mul_pos
Int
.
mul_lt_mul_of_pos_left
Int
.
mul_lt_mul_of_pos_right
Int
.
mul_le_mul_of_nonneg_left
Int
.
mul_le_mul_of_nonneg_right
Int
.
mul_le_mul
Int
.
mul_nonpos_of_nonneg_of_nonpos
Int
.
mul_nonpos_of_nonpos_of_nonneg
Int
.
mul_le_mul_of_nonpos_right
Int
.
mul_le_mul_of_nonpos_left
Int
.
natAbs_ofNat
Int
.
natAbs_negSucc
Int
.
natAbs_zero
Int
.
natAbs_one
Int
.
natAbs_eq_zero
Int
.
natAbs_pos
Int
.
natAbs_neg
Int
.
natAbs_eq
Int
.
natAbs_negOfNat
Int
.
natAbs_mul
Int
.
natAbs_eq_natAbs_iff
Int
.
natAbs_of_nonneg
Int
.
ofNat_natAbs_of_nonpos
Int
.
toNat_eq_max
Int
.
toNat_zero
Int
.
toNat_one
Int
.
toNat_of_nonneg
Int
.
toNat_ofNat
Int
.
toNat_negSucc
Int
.
toNat_ofNat_add_one
Int
.
ofNat_toNat
Int
.
self_le_toNat
Int
.
le_toNat
Int
.
toNat_lt
Int
.
toNat_add
Int
.
toNat_add_nat
Int
.
pred_toNat
Int
.
toNat_sub_toNat_neg
Int
.
toNat_add_toNat_neg_eq_natAbs
Int
.
toNat_neg_nat
Int
.
mem_toNat'
Int
.
le_of_not_le
Int
.
negSucc_not_pos
Int
.
eq_negSucc_of_lt_zero
Int
.
lt_of_add_lt_add_left
Int
.
lt_of_add_lt_add_right
Int
.
add_lt_add_iff_left
Int
.
add_lt_add_iff_right
Int
.
add_lt_add
Int
.
add_lt_add_of_le_of_lt
Int
.
add_lt_add_of_lt_of_le
Int
.
lt_add_of_pos_right
Int
.
lt_add_of_pos_left
Int
.
add_nonneg
Int
.
add_pos
Int
.
add_pos_of_pos_of_nonneg
Int
.
add_pos_of_nonneg_of_pos
Int
.
add_nonpos
Int
.
add_neg
Int
.
add_neg_of_neg_of_nonpos
Int
.
add_neg_of_nonpos_of_neg
Int
.
lt_add_of_le_of_pos
Int
.
add_one_le_iff
Int
.
lt_add_one_iff
Int
.
succ_ofNat_pos
Int
.
not_ofNat_neg
Int
.
le_add_one
Int
.
nonneg_of_neg_nonpos
Int
.
nonpos_of_neg_nonneg
Int
.
lt_of_neg_lt_neg
Int
.
pos_of_neg_neg
Int
.
neg_of_neg_pos
Int
.
le_neg_of_le_neg
Int
.
neg_le_of_neg_le
Int
.
lt_neg_of_lt_neg
Int
.
neg_lt_of_neg_lt
Int
.
sub_nonpos_of_le
Int
.
le_of_sub_nonpos
Int
.
sub_neg_of_lt
Int
.
lt_of_sub_neg
Int
.
add_le_of_le_neg_add
Int
.
le_neg_add_of_add_le
Int
.
add_le_of_le_sub_left
Int
.
le_sub_left_of_add_le
Int
.
add_le_of_le_sub_right
Int
.
le_sub_right_of_add_le
Int
.
le_add_of_neg_add_le
Int
.
neg_add_le_of_le_add
Int
.
le_add_of_sub_left_le
Int
.
le_add_of_sub_right_le
Int
.
sub_right_le_of_le_add
Int
.
le_add_of_neg_add_le_left
Int
.
neg_add_le_left_of_le_add
Int
.
le_add_of_neg_add_le_right
Int
.
neg_add_le_right_of_le_add
Int
.
le_add_of_neg_le_sub_left
Int
.
neg_le_sub_left_of_le_add
Int
.
le_add_of_neg_le_sub_right
Int
.
neg_le_sub_right_of_le_add
Int
.
sub_le_of_sub_le
Int
.
sub_le_sub_left
Int
.
sub_le_sub_right
Int
.
sub_le_sub
Int
.
add_lt_of_lt_neg_add
Int
.
lt_neg_add_of_add_lt
Int
.
add_lt_of_lt_sub_left
Int
.
lt_sub_left_of_add_lt
Int
.
add_lt_of_lt_sub_right
Int
.
lt_sub_right_of_add_lt
Int
.
lt_add_of_neg_add_lt
Int
.
neg_add_lt_of_lt_add
Int
.
lt_add_of_sub_left_lt
Int
.
sub_left_lt_of_lt_add
Int
.
lt_add_of_sub_right_lt
Int
.
sub_right_lt_of_lt_add
Int
.
lt_add_of_neg_add_lt_left
Int
.
neg_add_lt_left_of_lt_add
Int
.
lt_add_of_neg_add_lt_right
Int
.
neg_add_lt_right_of_lt_add
Int
.
lt_add_of_neg_lt_sub_left
Int
.
neg_lt_sub_left_of_lt_add
Int
.
lt_add_of_neg_lt_sub_right
Int
.
neg_lt_sub_right_of_lt_add
Int
.
add_lt_iff
Int
.
sub_lt_iff
Int
.
sub_lt_of_sub_lt
Int
.
sub_lt_sub_left
Int
.
sub_lt_sub_right
Int
.
sub_lt_sub
Int
.
lt_of_sub_lt_sub_left
Int
.
lt_of_sub_lt_sub_right
Int
.
sub_lt_sub_left_iff
Int
.
sub_lt_sub_right_iff
Int
.
sub_lt_sub_of_le_of_lt
Int
.
sub_lt_sub_of_lt_of_le
Int
.
add_le_add_three
Int
.
exists_eq_neg_ofNat
Int
.
lt_of_add_one_le
Int
.
lt_add_one_of_le
Int
.
le_of_lt_add_one
Int
.
sub_one_lt_of_le
Int
.
le_of_sub_one_lt
Int
.
le_sub_one_of_lt
Int
.
lt_of_le_sub_one
Int
.
mul_lt_mul
Int
.
mul_lt_mul'
Int
.
mul_neg_of_pos_of_neg
Int
.
mul_neg_of_neg_of_pos
Int
.
mul_nonneg_of_nonpos_of_nonpos
Int
.
mul_lt_mul_of_neg_left
Int
.
mul_lt_mul_of_neg_right
Int
.
mul_pos_of_neg_of_neg
Int
.
mul_self_le_mul_self
Int
.
mul_self_lt_mul_self
Int
.
sign_zero
Int
.
sign_one
Int
.
sign_neg_one
Int
.
sign_of_add_one
Int
.
sign_negSucc
Int
.
natAbs_sign
Int
.
natAbs_sign_of_nonzero
Int
.
sign_ofNat_of_nonzero
Int
.
sign_neg
Int
.
sign_mul_natAbs
Int
.
sign_mul
Int
.
sign_eq_one_of_pos
Int
.
sign_eq_neg_one_of_neg
Int
.
eq_zero_of_sign_eq_zero
Int
.
pos_of_sign_eq_one
Int
.
neg_of_sign_eq_neg_one
Int
.
sign_eq_one_iff_pos
Int
.
sign_eq_neg_one_iff_neg
Int
.
sign_eq_zero_iff_zero
Int
.
sign_sign
Int
.
sign_nonneg
Int
.
mul_sign
Int
.
natAbs_ne_zero
Int
.
natAbs_mul_self
Int
.
eq_nat_or_neg
Int
.
natAbs_mul_natAbs_eq
Int
.
natAbs_mul_self'
Int
.
natAbs_eq_iff
Int
.
natAbs_add_le
Int
.
natAbs_sub_le
Int
.
negSucc_eq'
Int
.
natAbs_lt_natAbs_of_nonneg_of_lt
Int
.
eq_natAbs_iff_mul_eq_zero
Results about the order properties of the integers, and the integers as an ordered ring.
#
Order properties of the integers
#
source
theorem
Int
.
nonneg_def
{a :
Int
}
:
a
.NonNeg
↔
∃ (
n
:
Nat
),
a
=
↑
n
source
theorem
Int
.
NonNeg
.
elim
{a :
Int
}
:
a
.NonNeg
→
∃ (
n
:
Nat
),
a
=
↑
n
source
theorem
Int
.
nonneg_or_nonneg_neg
(a :
Int
)
:
a
.NonNeg
∨
(
-
a
)
.NonNeg
source
theorem
Int
.
le_def
{a b :
Int
}
:
a
≤
b
↔
(
b
-
a
)
.NonNeg
source
theorem
Int
.
lt_iff_add_one_le
{a b :
Int
}
:
a
<
b
↔
a
+
1
≤
b
source
theorem
Int
.
le
.
intro_sub
{a b :
Int
}
(n :
Nat
)
(h :
b
-
a
=
↑
n
)
:
a
≤
b
source
theorem
Int
.
le
.
intro
{a b :
Int
}
(n :
Nat
)
(h :
a
+
↑
n
=
b
)
:
a
≤
b
source
theorem
Int
.
le
.
dest_sub
{a b :
Int
}
(h :
a
≤
b
)
:
∃ (
n
:
Nat
),
b
-
a
=
↑
n
source
theorem
Int
.
le
.
dest
{a b :
Int
}
(h :
a
≤
b
)
:
∃ (
n
:
Nat
),
a
+
↑
n
=
b
source
theorem
Int
.
le_total
(a b :
Int
)
:
a
≤
b
∨
b
≤
a
source
@[simp]
theorem
Int
.
ofNat_le
{m n :
Nat
}
:
↑
m
≤
↑
n
↔
m
≤
n
source
theorem
Int
.
ofNat_zero_le
(n :
Nat
)
:
0
≤
↑
n
source
theorem
Int
.
eq_ofNat_of_zero_le
{a :
Int
}
(h :
0
≤
a
)
:
∃ (
n
:
Nat
),
a
=
↑
n
source
theorem
Int
.
eq_succ_of_zero_lt
{a :
Int
}
(h :
0
<
a
)
:
∃ (
n
:
Nat
),
a
=
↑
n
.succ
source
theorem
Int
.
lt_add_succ
(a :
Int
)
(n :
Nat
)
:
a
<
a
+
↑
n
.succ
source
theorem
Int
.
lt
.
intro
{a b :
Int
}
{n :
Nat
}
(h :
a
+
↑
n
.succ
=
b
)
:
a
<
b
source
theorem
Int
.
lt
.
dest
{a b :
Int
}
(h :
a
<
b
)
:
∃ (
n
:
Nat
),
a
+
↑
n
.succ
=
b
source
@[simp]
theorem
Int
.
ofNat_lt
{n m :
Nat
}
:
↑
n
<
↑
m
↔
n
<
m
source
@[simp]
theorem
Int
.
ofNat_pos
{n :
Nat
}
:
0
<
↑
n
↔
0
<
n
source
theorem
Int
.
ofNat_nonneg
(n :
Nat
)
:
0
≤
↑
n
source
theorem
Int
.
ofNat_succ_pos
(n :
Nat
)
:
0
<
↑
n
.succ
source
@[simp]
theorem
Int
.
le_refl
(a :
Int
)
:
a
≤
a
source
theorem
Int
.
le_trans
{a b c :
Int
}
(h₁ :
a
≤
b
)
(h₂ :
b
≤
c
)
:
a
≤
c
source
theorem
Int
.
le_antisymm
{a b :
Int
}
(h₁ :
a
≤
b
)
(h₂ :
b
≤
a
)
:
a
=
b
source
@[simp]
theorem
Int
.
lt_irrefl
(a :
Int
)
:
¬
a
<
a
source
theorem
Int
.
ne_of_lt
{a b :
Int
}
(h :
a
<
b
)
:
a
≠
b
source
theorem
Int
.
ne_of_gt
{a b :
Int
}
(h :
b
<
a
)
:
a
≠
b
source
theorem
Int
.
le_of_lt
{a b :
Int
}
(h :
a
<
b
)
:
a
≤
b
source
theorem
Int
.
lt_iff_le_and_ne
{a b :
Int
}
:
a
<
b
↔
a
≤
b
∧
a
≠
b
source
theorem
Int
.
lt_succ
(a :
Int
)
:
a
<
a
+
1
source
theorem
Int
.
zero_lt_one
:
0
<
1
source
theorem
Int
.
lt_iff_le_not_le
{a b :
Int
}
:
a
<
b
↔
a
≤
b
∧
¬
b
≤
a
source
theorem
Int
.
lt_of_not_ge
{a b :
Int
}
(h :
¬
a
≤
b
)
:
b
<
a
source
theorem
Int
.
not_le_of_gt
{a b :
Int
}
(h :
b
<
a
)
:
¬
a
≤
b
source
theorem
Int
.
not_le
{a b :
Int
}
:
¬
a
≤
b
↔
b
<
a
source
theorem
Int
.
not_lt
{a b :
Int
}
:
¬
a
<
b
↔
b
≤
a
source
theorem
Int
.
lt_trichotomy
(a b :
Int
)
:
a
<
b
∨
a
=
b
∨
b
<
a
source
theorem
Int
.
ne_iff_lt_or_gt
{a b :
Int
}
:
a
≠
b
↔
a
<
b
∨
b
<
a
source
theorem
Int
.
lt_or_gt_of_ne
{a b :
Int
}
:
a
≠
b
→
a
<
b
∨
b
<
a
source
theorem
Int
.
eq_iff_le_and_ge
{x y :
Int
}
:
x
=
y
↔
x
≤
y
∧
y
≤
x
source
theorem
Int
.
lt_of_le_of_lt
{a b c :
Int
}
(h₁ :
a
≤
b
)
(h₂ :
b
<
c
)
:
a
<
c
source
theorem
Int
.
lt_of_lt_of_le
{a b c :
Int
}
(h₁ :
a
<
b
)
(h₂ :
b
≤
c
)
:
a
<
c
source
theorem
Int
.
lt_trans
{a b c :
Int
}
(h₁ :
a
<
b
)
(h₂ :
b
<
c
)
:
a
<
c
source
instance
Int
.
instTransLe
:
Trans
(fun (
x1
x2
:
Int
) =>
x1
≤
x2
)
(fun (
x1
x2
:
Int
) =>
x1
≤
x2
)
fun (
x1
x2
:
Int
) =>
x1
≤
x2
Equations
Int.instTransLe
=
{
trans
:=
⋯
}
source
instance
Int
.
instTransLtLe
:
Trans
(fun (
x1
x2
:
Int
) =>
x1
<
x2
)
(fun (
x1
x2
:
Int
) =>
x1
≤
x2
)
fun (
x1
x2
:
Int
) =>
x1
<
x2
Equations
Int.instTransLtLe
=
{
trans
:=
⋯
}
source
instance
Int
.
instTransLeLt
:
Trans
(fun (
x1
x2
:
Int
) =>
x1
≤
x2
)
(fun (
x1
x2
:
Int
) =>
x1
<
x2
)
fun (
x1
x2
:
Int
) =>
x1
<
x2
Equations
Int.instTransLeLt
=
{
trans
:=
⋯
}
source
instance
Int
.
instTransLt
:
Trans
(fun (
x1
x2
:
Int
) =>
x1
<
x2
)
(fun (
x1
x2
:
Int
) =>
x1
<
x2
)
fun (
x1
x2
:
Int
) =>
x1
<
x2
Equations
Int.instTransLt
=
{
trans
:=
⋯
}
source
theorem
Int
.
min_def
(n m :
Int
)
:
min
n
m
=
if
n
≤
m
then
n
else
m
source
theorem
Int
.
max_def
(n m :
Int
)
:
max
n
m
=
if
n
≤
m
then
m
else
n
source
theorem
Int
.
min_comm
(a b :
Int
)
:
min
a
b
=
min
b
a
source
instance
Int
.
instCommutativeMin
:
Std.Commutative
min
Equations
Int.instCommutativeMin
=
⋯
source
theorem
Int
.
min_le_right
(a b :
Int
)
:
min
a
b
≤
b
source
theorem
Int
.
min_le_left
(a b :
Int
)
:
min
a
b
≤
a
source
theorem
Int
.
min_eq_left
{a b :
Int
}
(h :
a
≤
b
)
:
min
a
b
=
a
source
theorem
Int
.
min_eq_right
{a b :
Int
}
(h :
b
≤
a
)
:
min
a
b
=
b
source
theorem
Int
.
le_min
{a b c :
Int
}
:
a
≤
min
b
c
↔
a
≤
b
∧
a
≤
c
source
theorem
Int
.
max_comm
(a b :
Int
)
:
max
a
b
=
max
b
a
source
instance
Int
.
instCommutativeMax
:
Std.Commutative
max
Equations
Int.instCommutativeMax
=
⋯
source
theorem
Int
.
le_max_left
(a b :
Int
)
:
a
≤
max
a
b
source
theorem
Int
.
le_max_right
(a b :
Int
)
:
b
≤
max
a
b
source
theorem
Int
.
max_le
{a b c :
Int
}
:
max
a
b
≤
c
↔
a
≤
c
∧
b
≤
c
source
theorem
Int
.
max_eq_right
{a b :
Int
}
(h :
a
≤
b
)
:
max
a
b
=
b
source
theorem
Int
.
max_eq_left
{a b :
Int
}
(h :
b
≤
a
)
:
max
a
b
=
a
source
theorem
Int
.
eq_natAbs_of_zero_le
{a :
Int
}
(h :
0
≤
a
)
:
a
=
↑
a
.natAbs
source
theorem
Int
.
le_natAbs
{a :
Int
}
:
a
≤
↑
a
.natAbs
source
theorem
Int
.
negSucc_lt_zero
(n :
Nat
)
:
Int.negSucc
n
<
0
source
theorem
Int
.
negSucc_le_zero
(n :
Nat
)
:
Int.negSucc
n
≤
0
source
@[simp]
theorem
Int
.
negSucc_not_nonneg
(n :
Nat
)
:
0
≤
Int.negSucc
n
↔
False
source
@[simp]
theorem
Int
.
ofNat_max_zero
(n :
Nat
)
:
max
(↑
n
)
0
=
↑
n
source
@[simp]
theorem
Int
.
zero_max_ofNat
(n :
Nat
)
:
max
0
↑
n
=
↑
n
source
@[simp]
theorem
Int
.
negSucc_max_zero
(n :
Nat
)
:
max
(
Int.negSucc
n
)
0
=
0
source
@[simp]
theorem
Int
.
zero_max_negSucc
(n :
Nat
)
:
max
0
(
Int.negSucc
n
)
=
0
source
theorem
Int
.
add_le_add_left
{a b :
Int
}
(h :
a
≤
b
)
(c :
Int
)
:
c
+
a
≤
c
+
b
source
theorem
Int
.
add_lt_add_left
{a b :
Int
}
(h :
a
<
b
)
(c :
Int
)
:
c
+
a
<
c
+
b
source
theorem
Int
.
add_le_add_right
{a b :
Int
}
(h :
a
≤
b
)
(c :
Int
)
:
a
+
c
≤
b
+
c
source
theorem
Int
.
add_lt_add_right
{a b :
Int
}
(h :
a
<
b
)
(c :
Int
)
:
a
+
c
<
b
+
c
source
theorem
Int
.
le_of_add_le_add_left
{a b c :
Int
}
(h :
a
+
b
≤
a
+
c
)
:
b
≤
c
source
theorem
Int
.
le_of_add_le_add_right
{a b c :
Int
}
(h :
a
+
b
≤
c
+
b
)
:
a
≤
c
source
theorem
Int
.
add_le_add_iff_left
{b c :
Int
}
(a :
Int
)
:
a
+
b
≤
a
+
c
↔
b
≤
c
source
theorem
Int
.
add_le_add_iff_right
{a b :
Int
}
(c :
Int
)
:
a
+
c
≤
b
+
c
↔
a
≤
b
source
theorem
Int
.
add_le_add
{a b c d :
Int
}
(h₁ :
a
≤
b
)
(h₂ :
c
≤
d
)
:
a
+
c
≤
b
+
d
source
theorem
Int
.
le_add_of_nonneg_right
{a b :
Int
}
(h :
0
≤
b
)
:
a
≤
a
+
b
source
theorem
Int
.
le_add_of_nonneg_left
{a b :
Int
}
(h :
0
≤
b
)
:
a
≤
b
+
a
source
theorem
Int
.
neg_le_neg
{a b :
Int
}
(h :
a
≤
b
)
:
-
b
≤
-
a
source
theorem
Int
.
le_of_neg_le_neg
{a b :
Int
}
(h :
-
b
≤
-
a
)
:
a
≤
b
source
theorem
Int
.
neg_nonpos_of_nonneg
{a :
Int
}
(h :
0
≤
a
)
:
-
a
≤
0
source
theorem
Int
.
neg_nonneg_of_nonpos
{a :
Int
}
(h :
a
≤
0
)
:
0
≤
-
a
source
theorem
Int
.
neg_lt_neg
{a b :
Int
}
(h :
a
<
b
)
:
-
b
<
-
a
source
theorem
Int
.
neg_neg_of_pos
{a :
Int
}
(h :
0
<
a
)
:
-
a
<
0
source
theorem
Int
.
neg_pos_of_neg
{a :
Int
}
(h :
a
<
0
)
:
0
<
-
a
source
theorem
Int
.
sub_nonneg_of_le
{a b :
Int
}
(h :
b
≤
a
)
:
0
≤
a
-
b
source
theorem
Int
.
le_of_sub_nonneg
{a b :
Int
}
(h :
0
≤
a
-
b
)
:
b
≤
a
source
theorem
Int
.
sub_pos_of_lt
{a b :
Int
}
(h :
b
<
a
)
:
0
<
a
-
b
source
theorem
Int
.
lt_of_sub_pos
{a b :
Int
}
(h :
0
<
a
-
b
)
:
b
<
a
source
theorem
Int
.
sub_left_le_of_le_add
{a b c :
Int
}
(h :
a
≤
b
+
c
)
:
a
-
b
≤
c
source
theorem
Int
.
sub_le_self
(a :
Int
)
{b :
Int
}
(h :
0
≤
b
)
:
a
-
b
≤
a
source
theorem
Int
.
sub_lt_self
(a :
Int
)
{b :
Int
}
(h :
0
<
b
)
:
a
-
b
<
a
source
theorem
Int
.
add_one_le_of_lt
{a b :
Int
}
(H :
a
<
b
)
:
a
+
1
≤
b
source
theorem
Int
.
mul_nonneg
{a b :
Int
}
(ha :
0
≤
a
)
(hb :
0
≤
b
)
:
0
≤
a
*
b
source
theorem
Int
.
mul_pos
{a b :
Int
}
(ha :
0
<
a
)
(hb :
0
<
b
)
:
0
<
a
*
b
source
theorem
Int
.
mul_lt_mul_of_pos_left
{a b c :
Int
}
(h₁ :
a
<
b
)
(h₂ :
0
<
c
)
:
c
*
a
<
c
*
b
source
theorem
Int
.
mul_lt_mul_of_pos_right
{a b c :
Int
}
(h₁ :
a
<
b
)
(h₂ :
0
<
c
)
:
a
*
c
<
b
*
c
source
theorem
Int
.
mul_le_mul_of_nonneg_left
{a b c :
Int
}
(h₁ :
a
≤
b
)
(h₂ :
0
≤
c
)
:
c
*
a
≤
c
*
b
source
theorem
Int
.
mul_le_mul_of_nonneg_right
{a b c :
Int
}
(h₁ :
a
≤
b
)
(h₂ :
0
≤
c
)
:
a
*
c
≤
b
*
c
source
theorem
Int
.
mul_le_mul
{a b c d :
Int
}
(hac :
a
≤
c
)
(hbd :
b
≤
d
)
(nn_b :
0
≤
b
)
(nn_c :
0
≤
c
)
:
a
*
b
≤
c
*
d
source
theorem
Int
.
mul_nonpos_of_nonneg_of_nonpos
{a b :
Int
}
(ha :
0
≤
a
)
(hb :
b
≤
0
)
:
a
*
b
≤
0
source
theorem
Int
.
mul_nonpos_of_nonpos_of_nonneg
{a b :
Int
}
(ha :
a
≤
0
)
(hb :
0
≤
b
)
:
a
*
b
≤
0
source
theorem
Int
.
mul_le_mul_of_nonpos_right
{a b c :
Int
}
(h :
b
≤
a
)
(hc :
c
≤
0
)
:
a
*
c
≤
b
*
c
source
theorem
Int
.
mul_le_mul_of_nonpos_left
{a b c :
Int
}
(ha :
a
≤
0
)
(h :
c
≤
b
)
:
a
*
b
≤
a
*
c
source
@[simp]
theorem
Int
.
natAbs_ofNat
(n :
Nat
)
:
(↑
n
)
.natAbs
=
n
source
@[simp]
theorem
Int
.
natAbs_negSucc
(n :
Nat
)
:
(
Int.negSucc
n
)
.natAbs
=
n
.succ
source
@[simp]
theorem
Int
.
natAbs_zero
:
Int.natAbs
0
=
0
source
@[simp]
theorem
Int
.
natAbs_one
:
Int.natAbs
1
=
1
source
@[simp]
theorem
Int
.
natAbs_eq_zero
{a :
Int
}
:
a
.natAbs
=
0
↔
a
=
0
source
theorem
Int
.
natAbs_pos
{a :
Int
}
:
0
<
a
.natAbs
↔
a
≠
0
source
@[simp]
theorem
Int
.
natAbs_neg
(a :
Int
)
:
(
-
a
)
.natAbs
=
a
.natAbs
source
theorem
Int
.
natAbs_eq
(a :
Int
)
:
a
=
↑
a
.natAbs
∨
a
=
-
↑
a
.natAbs
source
theorem
Int
.
natAbs_negOfNat
(n :
Nat
)
:
(
Int.negOfNat
n
)
.natAbs
=
n
source
theorem
Int
.
natAbs_mul
(a b :
Int
)
:
(
a
*
b
)
.natAbs
=
a
.natAbs
*
b
.natAbs
source
theorem
Int
.
natAbs_eq_natAbs_iff
{a b :
Int
}
:
a
.natAbs
=
b
.natAbs
↔
a
=
b
∨
a
=
-
b
source
theorem
Int
.
natAbs_of_nonneg
{a :
Int
}
(H :
0
≤
a
)
:
↑
a
.natAbs
=
a
source
theorem
Int
.
ofNat_natAbs_of_nonpos
{a :
Int
}
(H :
a
≤
0
)
:
↑
a
.natAbs
=
-
a
toNat
#
source
theorem
Int
.
toNat_eq_max
(a :
Int
)
:
↑
a
.toNat
=
max
a
0
source
@[simp]
theorem
Int
.
toNat_zero
:
Int.toNat
0
=
0
source
@[simp]
theorem
Int
.
toNat_one
:
Int.toNat
1
=
1
source
theorem
Int
.
toNat_of_nonneg
{a :
Int
}
(h :
0
≤
a
)
:
↑
a
.toNat
=
a
source
@[simp]
theorem
Int
.
toNat_ofNat
(n :
Nat
)
:
(↑
n
)
.toNat
=
n
source
@[simp]
theorem
Int
.
toNat_negSucc
(n :
Nat
)
:
(
Int.negSucc
n
)
.toNat
=
0
source
@[simp]
theorem
Int
.
toNat_ofNat_add_one
{n :
Nat
}
:
(
↑
n
+
1
)
.toNat
=
n
+
1
source
@[simp]
theorem
Int
.
ofNat_toNat
(a :
Int
)
:
↑
a
.toNat
=
max
a
0
source
theorem
Int
.
self_le_toNat
(a :
Int
)
:
a
≤
↑
a
.toNat
source
@[simp]
theorem
Int
.
le_toNat
{n :
Nat
}
{z :
Int
}
(h :
0
≤
z
)
:
n
≤
z
.toNat
↔
↑
n
≤
z
source
@[simp]
theorem
Int
.
toNat_lt
{n :
Nat
}
{z :
Int
}
(h :
0
≤
z
)
:
z
.toNat
<
n
↔
z
<
↑
n
source
theorem
Int
.
toNat_add
{a b :
Int
}
(ha :
0
≤
a
)
(hb :
0
≤
b
)
:
(
a
+
b
)
.toNat
=
a
.toNat
+
b
.toNat
source
theorem
Int
.
toNat_add_nat
{a :
Int
}
(ha :
0
≤
a
)
(n :
Nat
)
:
(
a
+
↑
n
)
.toNat
=
a
.toNat
+
n
source
@[simp]
theorem
Int
.
pred_toNat
(i :
Int
)
:
(
i
-
1
)
.toNat
=
i
.toNat
-
1
source
theorem
Int
.
toNat_sub_toNat_neg
(n :
Int
)
:
↑
n
.toNat
-
↑
(
-
n
)
.toNat
=
n
source
@[simp]
theorem
Int
.
toNat_add_toNat_neg_eq_natAbs
(n :
Int
)
:
n
.toNat
+
(
-
n
)
.toNat
=
n
.natAbs
source
@[simp]
theorem
Int
.
toNat_neg_nat
(n :
Nat
)
:
(
-
↑
n
)
.toNat
=
0
toNat'
#
source
theorem
Int
.
mem_toNat'
{a :
Int
}
{n :
Nat
}
:
a
.toNat'
=
some
n
↔
a
=
↑
n
Order properties of the integers
#
source
theorem
Int
.
le_of_not_le
{a b :
Int
}
:
¬
a
≤
b
→
b
≤
a
source
@[simp]
theorem
Int
.
negSucc_not_pos
(n :
Nat
)
:
0
<
Int.negSucc
n
↔
False
source
theorem
Int
.
eq_negSucc_of_lt_zero
{a :
Int
}
:
a
<
0
→
∃ (
n
:
Nat
),
a
=
Int.negSucc
n
source
theorem
Int
.
lt_of_add_lt_add_left
{a b c :
Int
}
(h :
a
+
b
<
a
+
c
)
:
b
<
c
source
theorem
Int
.
lt_of_add_lt_add_right
{a b c :
Int
}
(h :
a
+
b
<
c
+
b
)
:
a
<
c
source
theorem
Int
.
add_lt_add_iff_left
{b c :
Int
}
(a :
Int
)
:
a
+
b
<
a
+
c
↔
b
<
c
source
theorem
Int
.
add_lt_add_iff_right
{a b :
Int
}
(c :
Int
)
:
a
+
c
<
b
+
c
↔
a
<
b
source
theorem
Int
.
add_lt_add
{a b c d :
Int
}
(h₁ :
a
<
b
)
(h₂ :
c
<
d
)
:
a
+
c
<
b
+
d
source
theorem
Int
.
add_lt_add_of_le_of_lt
{a b c d :
Int
}
(h₁ :
a
≤
b
)
(h₂ :
c
<
d
)
:
a
+
c
<
b
+
d
source
theorem
Int
.
add_lt_add_of_lt_of_le
{a b c d :
Int
}
(h₁ :
a
<
b
)
(h₂ :
c
≤
d
)
:
a
+
c
<
b
+
d
source
theorem
Int
.
lt_add_of_pos_right
(a :
Int
)
{b :
Int
}
(h :
0
<
b
)
:
a
<
a
+
b
source
theorem
Int
.
lt_add_of_pos_left
(a :
Int
)
{b :
Int
}
(h :
0
<
b
)
:
a
<
b
+
a
source
theorem
Int
.
add_nonneg
{a b :
Int
}
(ha :
0
≤
a
)
(hb :
0
≤
b
)
:
0
≤
a
+
b
source
theorem
Int
.
add_pos
{a b :
Int
}
(ha :
0
<
a
)
(hb :
0
<
b
)
:
0
<
a
+
b
source
theorem
Int
.
add_pos_of_pos_of_nonneg
{a b :
Int
}
(ha :
0
<
a
)
(hb :
0
≤
b
)
:
0
<
a
+
b
source
theorem
Int
.
add_pos_of_nonneg_of_pos
{a b :
Int
}
(ha :
0
≤
a
)
(hb :
0
<
b
)
:
0
<
a
+
b
source
theorem
Int
.
add_nonpos
{a b :
Int
}
(ha :
a
≤
0
)
(hb :
b
≤
0
)
:
a
+
b
≤
0
source
theorem
Int
.
add_neg
{a b :
Int
}
(ha :
a
<
0
)
(hb :
b
<
0
)
:
a
+
b
<
0
source
theorem
Int
.
add_neg_of_neg_of_nonpos
{a b :
Int
}
(ha :
a
<
0
)
(hb :
b
≤
0
)
:
a
+
b
<
0
source
theorem
Int
.
add_neg_of_nonpos_of_neg
{a b :
Int
}
(ha :
a
≤
0
)
(hb :
b
<
0
)
:
a
+
b
<
0
source
theorem
Int
.
lt_add_of_le_of_pos
{a b c :
Int
}
(hbc :
b
≤
c
)
(ha :
0
<
a
)
:
b
<
c
+
a
source
theorem
Int
.
add_one_le_iff
{a b :
Int
}
:
a
+
1
≤
b
↔
a
<
b
source
theorem
Int
.
lt_add_one_iff
{a b :
Int
}
:
a
<
b
+
1
↔
a
≤
b
source
@[simp]
theorem
Int
.
succ_ofNat_pos
(n :
Nat
)
:
0
<
↑
n
+
1
source
theorem
Int
.
not_ofNat_neg
(n :
Nat
)
:
¬
↑
n
<
0
source
theorem
Int
.
le_add_one
{a b :
Int
}
(h :
a
≤
b
)
:
a
≤
b
+
1
source
theorem
Int
.
nonneg_of_neg_nonpos
{a :
Int
}
(h :
-
a
≤
0
)
:
0
≤
a
source
theorem
Int
.
nonpos_of_neg_nonneg
{a :
Int
}
(h :
0
≤
-
a
)
:
a
≤
0
source
theorem
Int
.
lt_of_neg_lt_neg
{a b :
Int
}
(h :
-
b
<
-
a
)
:
a
<
b
source
theorem
Int
.
pos_of_neg_neg
{a :
Int
}
(h :
-
a
<
0
)
:
0
<
a
source
theorem
Int
.
neg_of_neg_pos
{a :
Int
}
(h :
0
<
-
a
)
:
a
<
0
source
theorem
Int
.
le_neg_of_le_neg
{a b :
Int
}
(h :
a
≤
-
b
)
:
b
≤
-
a
source
theorem
Int
.
neg_le_of_neg_le
{a b :
Int
}
(h :
-
a
≤
b
)
:
-
b
≤
a
source
theorem
Int
.
lt_neg_of_lt_neg
{a b :
Int
}
(h :
a
<
-
b
)
:
b
<
-
a
source
theorem
Int
.
neg_lt_of_neg_lt
{a b :
Int
}
(h :
-
a
<
b
)
:
-
b
<
a
source
theorem
Int
.
sub_nonpos_of_le
{a b :
Int
}
(h :
a
≤
b
)
:
a
-
b
≤
0
source
theorem
Int
.
le_of_sub_nonpos
{a b :
Int
}
(h :
a
-
b
≤
0
)
:
a
≤
b
source
theorem
Int
.
sub_neg_of_lt
{a b :
Int
}
(h :
a
<
b
)
:
a
-
b
<
0
source
theorem
Int
.
lt_of_sub_neg
{a b :
Int
}
(h :
a
-
b
<
0
)
:
a
<
b
source
theorem
Int
.
add_le_of_le_neg_add
{a b c :
Int
}
(h :
b
≤
-
a
+
c
)
:
a
+
b
≤
c
source
theorem
Int
.
le_neg_add_of_add_le
{a b c :
Int
}
(h :
a
+
b
≤
c
)
:
b
≤
-
a
+
c
source
theorem
Int
.
add_le_of_le_sub_left
{a b c :
Int
}
(h :
b
≤
c
-
a
)
:
a
+
b
≤
c
source
theorem
Int
.
le_sub_left_of_add_le
{a b c :
Int
}
(h :
a
+
b
≤
c
)
:
b
≤
c
-
a
source
theorem
Int
.
add_le_of_le_sub_right
{a b c :
Int
}
(h :
a
≤
c
-
b
)
:
a
+
b
≤
c
source
theorem
Int
.
le_sub_right_of_add_le
{a b c :
Int
}
(h :
a
+
b
≤
c
)
:
a
≤
c
-
b
source
theorem
Int
.
le_add_of_neg_add_le
{a b c :
Int
}
(h :
-
b
+
a
≤
c
)
:
a
≤
b
+
c
source
theorem
Int
.
neg_add_le_of_le_add
{a b c :
Int
}
(h :
a
≤
b
+
c
)
:
-
b
+
a
≤
c
source
theorem
Int
.
le_add_of_sub_left_le
{a b c :
Int
}
(h :
a
-
b
≤
c
)
:
a
≤
b
+
c
source
theorem
Int
.
le_add_of_sub_right_le
{a b c :
Int
}
(h :
a
-
c
≤
b
)
:
a
≤
b
+
c
source
theorem
Int
.
sub_right_le_of_le_add
{a b c :
Int
}
(h :
a
≤
b
+
c
)
:
a
-
c
≤
b
source
theorem
Int
.
le_add_of_neg_add_le_left
{a b c :
Int
}
(h :
-
b
+
a
≤
c
)
:
a
≤
b
+
c
source
theorem
Int
.
neg_add_le_left_of_le_add
{a b c :
Int
}
(h :
a
≤
b
+
c
)
:
-
b
+
a
≤
c
source
theorem
Int
.
le_add_of_neg_add_le_right
{a b c :
Int
}
(h :
-
c
+
a
≤
b
)
:
a
≤
b
+
c
source
theorem
Int
.
neg_add_le_right_of_le_add
{a b c :
Int
}
(h :
a
≤
b
+
c
)
:
-
c
+
a
≤
b
source
theorem
Int
.
le_add_of_neg_le_sub_left
{a b c :
Int
}
(h :
-
a
≤
b
-
c
)
:
c
≤
a
+
b
source
theorem
Int
.
neg_le_sub_left_of_le_add
{a b c :
Int
}
(h :
c
≤
a
+
b
)
:
-
a
≤
b
-
c
source
theorem
Int
.
le_add_of_neg_le_sub_right
{a b c :
Int
}
(h :
-
b
≤
a
-
c
)
:
c
≤
a
+
b
source
theorem
Int
.
neg_le_sub_right_of_le_add
{a b c :
Int
}
(h :
c
≤
a
+
b
)
:
-
b
≤
a
-
c
source
theorem
Int
.
sub_le_of_sub_le
{a b c :
Int
}
(h :
a
-
b
≤
c
)
:
a
-
c
≤
b
source
theorem
Int
.
sub_le_sub_left
{a b :
Int
}
(h :
a
≤
b
)
(c :
Int
)
:
c
-
b
≤
c
-
a
source
theorem
Int
.
sub_le_sub_right
{a b :
Int
}
(h :
a
≤
b
)
(c :
Int
)
:
a
-
c
≤
b
-
c
source
theorem
Int
.
sub_le_sub
{a b c d :
Int
}
(hab :
a
≤
b
)
(hcd :
c
≤
d
)
:
a
-
d
≤
b
-
c
source
theorem
Int
.
add_lt_of_lt_neg_add
{a b c :
Int
}
(h :
b
<
-
a
+
c
)
:
a
+
b
<
c
source
theorem
Int
.
lt_neg_add_of_add_lt
{a b c :
Int
}
(h :
a
+
b
<
c
)
:
b
<
-
a
+
c
source
theorem
Int
.
add_lt_of_lt_sub_left
{a b c :
Int
}
(h :
b
<
c
-
a
)
:
a
+
b
<
c
source
theorem
Int
.
lt_sub_left_of_add_lt
{a b c :
Int
}
(h :
a
+
b
<
c
)
:
b
<
c
-
a
source
theorem
Int
.
add_lt_of_lt_sub_right
{a b c :
Int
}
(h :
a
<
c
-
b
)
:
a
+
b
<
c
source
theorem
Int
.
lt_sub_right_of_add_lt
{a b c :
Int
}
(h :
a
+
b
<
c
)
:
a
<
c
-
b
source
theorem
Int
.
lt_add_of_neg_add_lt
{a b c :
Int
}
(h :
-
b
+
a
<
c
)
:
a
<
b
+
c
source
theorem
Int
.
neg_add_lt_of_lt_add
{a b c :
Int
}
(h :
a
<
b
+
c
)
:
-
b
+
a
<
c
source
theorem
Int
.
lt_add_of_sub_left_lt
{a b c :
Int
}
(h :
a
-
b
<
c
)
:
a
<
b
+
c
source
theorem
Int
.
sub_left_lt_of_lt_add
{a b c :
Int
}
(h :
a
<
b
+
c
)
:
a
-
b
<
c
source
theorem
Int
.
lt_add_of_sub_right_lt
{a b c :
Int
}
(h :
a
-
c
<
b
)
:
a
<
b
+
c
source
theorem
Int
.
sub_right_lt_of_lt_add
{a b c :
Int
}
(h :
a
<
b
+
c
)
:
a
-
c
<
b
source
theorem
Int
.
lt_add_of_neg_add_lt_left
{a b c :
Int
}
(h :
-
b
+
a
<
c
)
:
a
<
b
+
c
source
theorem
Int
.
neg_add_lt_left_of_lt_add
{a b c :
Int
}
(h :
a
<
b
+
c
)
:
-
b
+
a
<
c
source
theorem
Int
.
lt_add_of_neg_add_lt_right
{a b c :
Int
}
(h :
-
c
+
a
<
b
)
:
a
<
b
+
c
source
theorem
Int
.
neg_add_lt_right_of_lt_add
{a b c :
Int
}
(h :
a
<
b
+
c
)
:
-
c
+
a
<
b
source
theorem
Int
.
lt_add_of_neg_lt_sub_left
{a b c :
Int
}
(h :
-
a
<
b
-
c
)
:
c
<
a
+
b
source
theorem
Int
.
neg_lt_sub_left_of_lt_add
{a b c :
Int
}
(h :
c
<
a
+
b
)
:
-
a
<
b
-
c
source
theorem
Int
.
lt_add_of_neg_lt_sub_right
{a b c :
Int
}
(h :
-
b
<
a
-
c
)
:
c
<
a
+
b
source
theorem
Int
.
neg_lt_sub_right_of_lt_add
{a b c :
Int
}
(h :
c
<
a
+
b
)
:
-
b
<
a
-
c
source
theorem
Int
.
add_lt_iff
{a b c :
Int
}
:
a
+
b
<
c
↔
a
<
-
b
+
c
source
theorem
Int
.
sub_lt_iff
{a b c :
Int
}
:
a
-
b
<
c
↔
a
<
c
+
b
source
theorem
Int
.
sub_lt_of_sub_lt
{a b c :
Int
}
(h :
a
-
b
<
c
)
:
a
-
c
<
b
source
theorem
Int
.
sub_lt_sub_left
{a b :
Int
}
(h :
a
<
b
)
(c :
Int
)
:
c
-
b
<
c
-
a
source
theorem
Int
.
sub_lt_sub_right
{a b :
Int
}
(h :
a
<
b
)
(c :
Int
)
:
a
-
c
<
b
-
c
source
theorem
Int
.
sub_lt_sub
{a b c d :
Int
}
(hab :
a
<
b
)
(hcd :
c
<
d
)
:
a
-
d
<
b
-
c
source
theorem
Int
.
lt_of_sub_lt_sub_left
{a b c :
Int
}
(h :
c
-
a
<
c
-
b
)
:
b
<
a
source
theorem
Int
.
lt_of_sub_lt_sub_right
{a b c :
Int
}
(h :
a
-
c
<
b
-
c
)
:
a
<
b
source
@[simp]
theorem
Int
.
sub_lt_sub_left_iff
{a b c :
Int
}
:
c
-
a
<
c
-
b
↔
b
<
a
source
@[simp]
theorem
Int
.
sub_lt_sub_right_iff
{a b c :
Int
}
:
a
-
c
<
b
-
c
↔
a
<
b
source
theorem
Int
.
sub_lt_sub_of_le_of_lt
{a b c d :
Int
}
(hab :
a
≤
b
)
(hcd :
c
<
d
)
:
a
-
d
<
b
-
c
source
theorem
Int
.
sub_lt_sub_of_lt_of_le
{a b c d :
Int
}
(hab :
a
<
b
)
(hcd :
c
≤
d
)
:
a
-
d
<
b
-
c
source
theorem
Int
.
add_le_add_three
{a b c d e f :
Int
}
(h₁ :
a
≤
d
)
(h₂ :
b
≤
e
)
(h₃ :
c
≤
f
)
:
a
+
b
+
c
≤
d
+
e
+
f
source
theorem
Int
.
exists_eq_neg_ofNat
{a :
Int
}
(H :
a
≤
0
)
:
∃ (
n
:
Nat
),
a
=
-
↑
n
source
theorem
Int
.
lt_of_add_one_le
{a b :
Int
}
(H :
a
+
1
≤
b
)
:
a
<
b
source
theorem
Int
.
lt_add_one_of_le
{a b :
Int
}
(H :
a
≤
b
)
:
a
<
b
+
1
source
theorem
Int
.
le_of_lt_add_one
{a b :
Int
}
(H :
a
<
b
+
1
)
:
a
≤
b
source
theorem
Int
.
sub_one_lt_of_le
{a b :
Int
}
(H :
a
≤
b
)
:
a
-
1
<
b
source
theorem
Int
.
le_of_sub_one_lt
{a b :
Int
}
(H :
a
-
1
<
b
)
:
a
≤
b
source
theorem
Int
.
le_sub_one_of_lt
{a b :
Int
}
(H :
a
<
b
)
:
a
≤
b
-
1
source
theorem
Int
.
lt_of_le_sub_one
{a b :
Int
}
(H :
a
≤
b
-
1
)
:
a
<
b
source
theorem
Int
.
mul_lt_mul
{a b c d :
Int
}
(h₁ :
a
<
c
)
(h₂ :
b
≤
d
)
(h₃ :
0
<
b
)
(h₄ :
0
≤
c
)
:
a
*
b
<
c
*
d
source
theorem
Int
.
mul_lt_mul'
{a b c d :
Int
}
(h₁ :
a
≤
c
)
(h₂ :
b
<
d
)
(h₃ :
0
≤
b
)
(h₄ :
0
<
c
)
:
a
*
b
<
c
*
d
source
theorem
Int
.
mul_neg_of_pos_of_neg
{a b :
Int
}
(ha :
0
<
a
)
(hb :
b
<
0
)
:
a
*
b
<
0
source
theorem
Int
.
mul_neg_of_neg_of_pos
{a b :
Int
}
(ha :
a
<
0
)
(hb :
0
<
b
)
:
a
*
b
<
0
source
theorem
Int
.
mul_nonneg_of_nonpos_of_nonpos
{a b :
Int
}
(ha :
a
≤
0
)
(hb :
b
≤
0
)
:
0
≤
a
*
b
source
theorem
Int
.
mul_lt_mul_of_neg_left
{a b c :
Int
}
(h :
b
<
a
)
(hc :
c
<
0
)
:
c
*
a
<
c
*
b
source
theorem
Int
.
mul_lt_mul_of_neg_right
{a b c :
Int
}
(h :
b
<
a
)
(hc :
c
<
0
)
:
a
*
c
<
b
*
c
source
theorem
Int
.
mul_pos_of_neg_of_neg
{a b :
Int
}
(ha :
a
<
0
)
(hb :
b
<
0
)
:
0
<
a
*
b
source
theorem
Int
.
mul_self_le_mul_self
{a b :
Int
}
(h1 :
0
≤
a
)
(h2 :
a
≤
b
)
:
a
*
a
≤
b
*
b
source
theorem
Int
.
mul_self_lt_mul_self
{a b :
Int
}
(h1 :
0
≤
a
)
(h2 :
a
<
b
)
:
a
*
a
<
b
*
b
source
@[simp]
theorem
Int
.
sign_zero
:
Int.sign
0
=
0
source
@[simp]
theorem
Int
.
sign_one
:
Int.sign
1
=
1
source
theorem
Int
.
sign_neg_one
:
(-
1
)
.sign
=
-
1
source
@[simp]
theorem
Int
.
sign_of_add_one
(x :
Nat
)
:
(
↑
x
+
1
)
.sign
=
1
source
@[simp]
theorem
Int
.
sign_negSucc
(x :
Nat
)
:
(
Int.negSucc
x
)
.sign
=
-
1
source
theorem
Int
.
natAbs_sign
(z :
Int
)
:
z
.sign
.natAbs
=
if
z
=
0
then
0
else
1
source
theorem
Int
.
natAbs_sign_of_nonzero
{z :
Int
}
(hz :
z
≠
0
)
:
z
.sign
.natAbs
=
1
source
theorem
Int
.
sign_ofNat_of_nonzero
{n :
Nat
}
(hn :
n
≠
0
)
:
(↑
n
)
.sign
=
1
source
@[simp]
theorem
Int
.
sign_neg
(z :
Int
)
:
(
-
z
)
.sign
=
-
z
.sign
source
theorem
Int
.
sign_mul_natAbs
(a :
Int
)
:
a
.sign
*
↑
a
.natAbs
=
a
source
@[simp]
theorem
Int
.
sign_mul
(a b :
Int
)
:
(
a
*
b
)
.sign
=
a
.sign
*
b
.sign
source
theorem
Int
.
sign_eq_one_of_pos
{a :
Int
}
(h :
0
<
a
)
:
a
.sign
=
1
source
theorem
Int
.
sign_eq_neg_one_of_neg
{a :
Int
}
(h :
a
<
0
)
:
a
.sign
=
-
1
source
theorem
Int
.
eq_zero_of_sign_eq_zero
{a :
Int
}
:
a
.sign
=
0
→
a
=
0
source
theorem
Int
.
pos_of_sign_eq_one
{a :
Int
}
:
a
.sign
=
1
→
0
<
a
source
theorem
Int
.
neg_of_sign_eq_neg_one
{a :
Int
}
:
a
.sign
=
-
1
→
a
<
0
source
theorem
Int
.
sign_eq_one_iff_pos
{a :
Int
}
:
a
.sign
=
1
↔
0
<
a
source
theorem
Int
.
sign_eq_neg_one_iff_neg
{a :
Int
}
:
a
.sign
=
-
1
↔
a
<
0
source
@[simp]
theorem
Int
.
sign_eq_zero_iff_zero
{a :
Int
}
:
a
.sign
=
0
↔
a
=
0
source
@[simp]
theorem
Int
.
sign_sign
{x :
Int
}
:
x
.sign
.sign
=
x
.sign
source
@[simp]
theorem
Int
.
sign_nonneg
{x :
Int
}
:
0
≤
x
.sign
↔
0
≤
x
source
theorem
Int
.
mul_sign
(i :
Int
)
:
i
*
i
.sign
=
↑
i
.natAbs
source
theorem
Int
.
natAbs_ne_zero
{a :
Int
}
:
a
.natAbs
≠
0
↔
a
≠
0
source
theorem
Int
.
natAbs_mul_self
{a :
Int
}
:
↑
(
a
.natAbs
*
a
.natAbs
)
=
a
*
a
source
theorem
Int
.
eq_nat_or_neg
(a :
Int
)
:
∃ (
n
:
Nat
),
a
=
↑
n
∨
a
=
-
↑
n
source
theorem
Int
.
natAbs_mul_natAbs_eq
{a b :
Int
}
{c :
Nat
}
(h :
a
*
b
=
↑
c
)
:
a
.natAbs
*
b
.natAbs
=
c
source
@[simp]
theorem
Int
.
natAbs_mul_self'
(a :
Int
)
:
↑
a
.natAbs
*
↑
a
.natAbs
=
a
*
a
source
theorem
Int
.
natAbs_eq_iff
{a :
Int
}
{n :
Nat
}
:
a
.natAbs
=
n
↔
a
=
↑
n
∨
a
=
-
↑
n
source
theorem
Int
.
natAbs_add_le
(a b :
Int
)
:
(
a
+
b
)
.natAbs
≤
a
.natAbs
+
b
.natAbs
source
theorem
Int
.
natAbs_sub_le
(a b :
Int
)
:
(
a
-
b
)
.natAbs
≤
a
.natAbs
+
b
.natAbs
source
theorem
Int
.
negSucc_eq'
(m :
Nat
)
:
Int.negSucc
m
=
-
↑
m
-
1
source
theorem
Int
.
natAbs_lt_natAbs_of_nonneg_of_lt
{a b :
Int
}
(w₁ :
0
≤
a
)
(w₂ :
a
<
b
)
:
a
.natAbs
<
b
.natAbs
source
theorem
Int
.
eq_natAbs_iff_mul_eq_zero
{a :
Int
}
{n :
Nat
}
:
a
.natAbs
=
n
↔
(
a
-
↑
n
)
*
(
a
+
↑
n
)
=
0