# Documentation

Mathlib.Data.Int.Order.Basic

# Order instances on the integers #

This file contains:

• instances on ℤ. The stronger one is Int.linearOrderedCommRing.
• basic lemmas about integers that involve order properties.

## Recursors #

• Int.rec: Sign disjunction. Something is true/defined on ℤ if it's true/defined for nonnegative and for negative values. (Defined in core Lean 3)
• Int.inductionOn: Simple growing induction on positive numbers, plus simple decreasing induction on negative numbers. Note that this recursor is currently only Prop-valued.
• Int.inductionOn': Simple growing induction for numbers greater than b, plus simple decreasing induction on numbers less than b.

### Extra instances to short-circuit type class resolution #

theorem Int.abs_eq_natAbs (a : ) :
|a| = ↑()
@[simp]
theorem Int.coe_natAbs (n : ) :
↑() = |n|
theorem Nat.cast_natAbs {α : Type u_1} [] (n : ) :
↑() = |n|
theorem Int.natAbs_abs (a : ) :
theorem Int.sign_mul_abs (a : ) :
* |a| = a
theorem Int.coe_nat_eq_zero {n : } :
n = 0 n = 0
theorem Int.coe_nat_ne_zero {n : } :
n 0 n 0
theorem Int.coe_nat_ne_zero_iff_pos {n : } :
n 0 0 < n
theorem Int.abs_coe_nat (n : ) :
|n| = n
theorem Int.sign_add_eq_of_sign_eq {m : } {n : } :
Int.sign (m + n) =

### succ and pred #

theorem Int.lt_succ_self (a : ) :
a <
theorem Int.pred_self_lt (a : ) :
< a
theorem Int.sub_one_lt_iff {a : } {b : } :
a - 1 < b a b
theorem Int.le_sub_one_iff {a : } {b : } :
a b - 1 a < b
@[simp]
theorem Int.abs_lt_one_iff {a : } :
|a| < 1 a = 0
theorem Int.abs_le_one_iff {a : } :
|a| 1 a = 0 a = 1 a = -1
theorem Int.one_le_abs {z : } (h₀ : z 0) :
1 |z|
def Int.inductionOn' {C : Sort u_1} (z : ) (b : ) (H0 : C b) (Hs : (k : ) → b kC kC (k + 1)) (Hp : (k : ) → k bC kC (k - 1)) :
C z

Inductively define a function on ℤ by defining it at b, for the succ of a number greater than b, and the pred of a number less than b.

Instances For
def Int.inductionOn'.pos {C : Sort u_1} (b : ) (H0 : C b) (Hs : (k : ) → b kC kC (k + 1)) (n : ) :
C (b + n)

The positive case of Int.inductionOn'.

Equations
Instances For
def Int.inductionOn'.neg {C : Sort u_1} (b : ) (H0 : C b) (Hp : (k : ) → k bC kC (k - 1)) (n : ) :
C (b + )

The negative case of Int.inductionOn'.

Equations
Instances For
theorem Int.le_induction {P : } {m : } (h0 : P m) (h1 : (n : ) → m nP nP (n + 1)) (n : ) :
m nP n

See Int.inductionOn' for an induction in both directions.

theorem Int.le_induction_down {P : } {m : } (h0 : P m) (h1 : (n : ) → n mP nP (n - 1)) (n : ) :
n mP n

See Int.inductionOn' for an induction in both directions.

### /#

theorem Int.ediv_eq_zero_of_lt_abs {a : } {b : } (H1 : 0 a) (H2 : a < |b|) :
a / b = 0

### mod #

@[simp]
theorem Int.emod_abs (a : ) (b : ) :
a % |b| = a % b
theorem Int.emod_lt (a : ) {b : } (H : b 0) :
a % b < |b|
theorem Int.add_emod_eq_add_mod_right {m : } {n : } {k : } (i : ) (H : m % n = k % n) :
(m + i) % n = (k + i) % n
@[simp]
theorem Int.neg_emod_two (i : ) :
-i % 2 = i % 2

### properties of / and %#

theorem Int.abs_ediv_le_abs (a : ) (b : ) :
|a / b| |a|
theorem Int.emod_two_eq_zero_or_one (n : ) :
n % 2 = 0 n % 2 = 1

### dvd #

theorem Int.ediv_dvd_ediv {a : } {b : } {c : } :
a bb cb / a c / a
theorem Int.abs_sign_of_nonzero {z : } (hz : z 0) :
|| = 1
theorem Int.exists_lt_and_lt_iff_not_dvd (m : ) {n : } (hn : 0 < n) :
(k, n * k < m m < n * (k + 1)) ¬n m

If n > 0 then m is not divisible by n iff it is between n * k and n * (k + 1) for some k.

theorem Int.sign_eq_ediv_abs (a : ) :
= a / |a|

### / and ordering #

theorem Int.ediv_mul_le (a : ) {b : } (H : b 0) :
a / b * b a
theorem Int.ediv_le_of_le_mul {a : } {b : } {c : } (H : 0 < c) (H' : a b * c) :
a / c b
theorem Int.mul_lt_of_lt_ediv {a : } {b : } {c : } (H : 0 < c) (H3 : a < b / c) :
a * c < b
theorem Int.mul_le_of_le_ediv {a : } {b : } {c : } (H1 : 0 < c) (H2 : a b / c) :
a * c b
theorem Int.le_ediv_of_mul_le {a : } {b : } {c : } (H1 : 0 < c) (H2 : a * c b) :
a b / c
theorem Int.le_ediv_iff_mul_le {a : } {b : } {c : } (H : 0 < c) :
a b / c a * c b
theorem Int.ediv_le_ediv {a : } {b : } {c : } (H : 0 < c) (H' : a b) :
a / c b / c
theorem Int.ediv_lt_of_lt_mul {a : } {b : } {c : } (H : 0 < c) (H' : a < b * c) :
a / c < b
theorem Int.lt_mul_of_ediv_lt {a : } {b : } {c : } (H1 : 0 < c) (H2 : a / c < b) :
a < b * c
theorem Int.ediv_lt_iff_lt_mul {a : } {b : } {c : } (H : 0 < c) :
a / c < b a < b * c
theorem Int.le_mul_of_ediv_le {a : } {b : } {c : } (H1 : 0 b) (H2 : b a) (H3 : a / b c) :
a c * b
theorem Int.lt_ediv_of_mul_lt {a : } {b : } {c : } (H1 : 0 b) (H2 : b c) (H3 : a * b < c) :
a < c / b
theorem Int.lt_ediv_iff_mul_lt {a : } {b : } (c : ) (H : 0 < c) (H' : c b) :
a < b / c a * c < b
theorem Int.ediv_pos_of_pos_of_dvd {a : } {b : } (H1 : 0 < a) (H2 : 0 b) (H3 : b a) :
0 < a / b
theorem Int.natAbs_eq_of_dvd_dvd {s : } {t : } (hst : s t) (hts : t s) :
theorem Int.ediv_eq_ediv_of_mul_eq_mul {a : } {b : } {c : } {d : } (H2 : d c) (H3 : b 0) (H4 : d 0) (H5 : a * d = b * c) :
a / b = c / d
theorem Int.ediv_dvd_of_dvd {s : } {t : } (hst : s t) :
t / s t

### toNat #

@[simp]
theorem Int.toNat_le {a : } {n : } :
n a n
@[simp]
theorem Int.lt_toNat {n : } {a : } :
n < n < a
@[simp]
theorem Int.coe_nat_nonpos_iff {n : } :
n 0 n = 0
theorem Int.toNat_le_toNat {a : } {b : } (h : a b) :
theorem Int.toNat_lt_toNat {a : } {b : } (hb : 0 < b) :
a < b
theorem Int.lt_of_toNat_lt {a : } {b : } (h : ) :
a < b
@[simp]
theorem Int.toNat_pred_coe_of_pos {i : } (h : 0 < i) :
↑( - 1) = i - 1
@[simp]
theorem Int.toNat_eq_zero {n : } :
= 0 n 0
@[simp]
theorem Int.toNat_sub_of_le {a : } {b : } (h : b a) :
↑(Int.toNat (a - b)) = a - b