# mathlib3documentation

data.nat.order.basic

# The natural numbers as a linearly ordered commutative semiring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We also have a variety of lemmas which have been deferred from data.nat.basic because it is easier to prove them with this ordered semiring instance available.

You may find that some theorems can be moved back to data.nat.basic by modifying their proofs.

### instances #

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

Extra instances to short-circuit type class resolution and ensure computability

@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations

### Equalities and inequalities involving zero and one #

theorem nat.one_le_iff_ne_zero {n : } :
1 n n 0
theorem nat.one_lt_iff_ne_zero_and_ne_one {n : } :
1 < n n 0 n 1
@[protected]
theorem nat.mul_ne_zero {m n : } (n0 : n 0) (m0 : m 0) :
n * m 0
@[protected, simp]
theorem nat.mul_eq_zero {m n : } :
m * n = 0 m = 0 n = 0
@[protected, simp]
theorem nat.zero_eq_mul {m n : } :
0 = m * n m = 0 n = 0
theorem nat.eq_zero_of_double_le {n : } (h : 2 * n n) :
n = 0
theorem nat.eq_zero_of_mul_le {m n : } (hb : 2 n) (h : n * m m) :
m = 0
theorem nat.zero_max {n : } :
= n
@[simp]
theorem nat.min_eq_zero_iff {m n : } :
= 0 m = 0 n = 0
@[simp]
theorem nat.max_eq_zero_iff {m n : } :
= 0 m = 0 n = 0
theorem nat.add_eq_max_iff {m n : } :
m + n = m = 0 n = 0
theorem nat.add_eq_min_iff {m n : } :
m + n = m = 0 n = 0
theorem nat.one_le_of_lt {m n : } (h : n < m) :
1 m
theorem nat.eq_one_of_mul_eq_one_right {m n : } (H : m * n = 1) :
m = 1
theorem nat.eq_one_of_mul_eq_one_left {m n : } (H : m * n = 1) :
n = 1

### succ#

theorem nat.two_le_iff (n : ) :
2 n n 0 n 1
@[simp]
theorem nat.lt_one_iff {n : } :
n < 1 n = 0

### add#

theorem nat.add_pos_left {m : } (h : 0 < m) (n : ) :
0 < m + n
theorem nat.add_pos_right (m : ) {n : } (h : 0 < n) :
0 < m + n
theorem nat.add_pos_iff_pos_or_pos (m n : ) :
0 < m + n 0 < m 0 < n
theorem nat.add_eq_one_iff {m n : } :
m + n = 1 m = 0 n = 1 m = 1 n = 0
theorem nat.add_eq_two_iff {m n : } :
m + n = 2 m = 0 n = 2 m = 1 n = 1 m = 2 n = 0
theorem nat.add_eq_three_iff {m n : } :
m + n = 3 m = 0 n = 3 m = 1 n = 2 m = 2 n = 1 m = 3 n = 0
theorem nat.le_add_one_iff {m n : } :
m n + 1 m n m = n + 1
theorem nat.le_and_le_add_one_iff {m n : } :
n m m n + 1 m = n m = n + 1
theorem nat.add_succ_lt_add {m n k l : } (hab : m < n) (hcd : k < l) :
m + k + 1 < n + l

### pred#

theorem nat.pred_le_iff {m n : } :
m.pred n m n.succ

### sub#

Most lemmas come from the has_ordered_sub instance on ℕ.

@[protected, instance]
theorem nat.lt_pred_iff {m n : } :
n < m.pred n.succ < m
theorem nat.lt_of_lt_pred {m n : } (h : m < n - 1) :
m < n
theorem nat.le_or_le_of_add_eq_add_pred {m n k l : } (h : k + l = m + n - 1) :
m k n l
theorem nat.sub_succ' (m n : ) :
m - n.succ = m - n - 1

A version of nat.sub_succ in the form _ - 1 instead of nat.pred _.

### mul#

theorem nat.succ_mul_pos {n : } (m : ) (hn : 0 < n) :
0 < m.succ * n
theorem nat.mul_self_le_mul_self {m n : } (h : m n) :
m * m n * n
theorem nat.mul_self_lt_mul_self {m n : } :
m < n m * m < n * n
theorem nat.mul_self_le_mul_self_iff {m n : } :
m n m * m n * n
theorem nat.mul_self_lt_mul_self_iff {m n : } :
m < n m * m < n * n
theorem nat.le_mul_self (n : ) :
n n * n
theorem nat.le_mul_of_pos_left {m n : } (h : 0 < n) :
m n * m
theorem nat.le_mul_of_pos_right {m n : } (h : 0 < n) :
m m * n
theorem nat.mul_self_inj {m n : } :
m * m = n * n m = n
theorem nat.le_add_pred_of_pos (n : ) {i : } (hi : i 0) :
n i + (n - 1)
@[simp]
theorem nat.lt_mul_self_iff {n : } :
n < n * n 1 < n
theorem nat.add_sub_one_le_mul {m n : } (hm : m 0) (hn : n 0) :
m + n - 1 m * n

### Recursion and induction principles #

This section is here due to dependencies -- the lemmas here require some of the lemmas proved above, and some of the results in later sections depend on the definitions in this section.

theorem nat.diag_induction (P : Prop) (ha : (a : ), P (a + 1) (a + 1)) (hb : (b : ), P 0 (b + 1)) (hd : (a b : ), a < b P (a + 1) b P a (b + 1) P (a + 1) (b + 1)) (a b : ) :
a < b P a b

Given a predicate on two naturals P : ℕ → ℕ → Prop, P a b is true for all a < b if P (a + 1) (a + 1) is true for all a, P 0 (b + 1) is true for all b and for all a < b, P (a + 1) b is true and P a (b + 1) is true implies P (a + 1) (b + 1) is true.

theorem nat.set_induction_bounded {n k : } {S : set } (hk : k S) (h_ind : (k : ), k S k + 1 S) (hnk : k n) :
n S

A subset of ℕ containing k : ℕ and closed under nat.succ contains every n ≥ k.

theorem nat.set_induction {S : set } (hb : 0 S) (h_ind : (k : ), k S k + 1 S) (n : ) :
n S

A subset of ℕ containing zero and closed under nat.succ contains all of ℕ.

### div#

@[protected]
theorem nat.div_le_of_le_mul' {m n k : } (h : m k * n) :
m / k n
@[protected]
theorem nat.div_le_self' (m n : ) :
m / n m
@[protected]
theorem nat.div_lt_of_lt_mul {m n k : } (h : m < n * k) :
m / n < k
theorem nat.eq_zero_of_le_div {m n : } (hn : 2 n) (h : m m / n) :
m = 0
theorem nat.div_mul_div_le_div (m n k : ) :
m / k * n / m n / k
theorem nat.eq_zero_of_le_half {n : } (h : n n / 2) :
n = 0
theorem nat.mul_div_mul_comm_of_dvd_dvd {m n k l : } (hmk : k m) (hnl : l n) :
m * n / (k * l) = m / k * (n / l)
theorem nat.le_half_of_half_lt_sub {a b : } (h : a / 2 < a - b) :
b a / 2
theorem nat.half_le_of_sub_le_half {a b : } (h : a - b a / 2) :
a / 2 b

### mod, dvd#

theorem nat.two_mul_odd_div_two {n : } (hn : n % 2 = 1) :
2 * (n / 2) = n - 1
theorem nat.div_dvd_of_dvd {m n : } (h : n m) :
m / n m
@[protected]
theorem nat.div_div_self {m n : } (h : n m) (hm : m 0) :
m / (m / n) = n
theorem nat.mod_mul_right_div_self (m n k : ) :
m % (n * k) / n = m / n % k
theorem nat.mod_mul_left_div_self (m n k : ) :
m % (k * n) / n = m / n % k
theorem nat.not_dvd_of_pos_of_lt {m n : } (h1 : 0 < n) (h2 : n < m) :
¬m n
theorem nat.sub_mod_eq_zero_of_mod_eq {m n k : } (h : m % k = n % k) :
(m - n) % k = 0

If m and n are equal mod k, m - n is zero mod k.

@[simp]
theorem nat.one_mod (n : ) :
1 % (n + 2) = 1
theorem nat.dvd_sub_mod {n : } (k : ) :
n k - k % n
theorem nat.add_mod_eq_ite {m n k : } :
(m + n) % k = ite (k m % k + n % k) (m % k + n % k - k) (m % k + n % k)
theorem nat.div_mul_div_comm {m n k l : } (hmn : n m) (hkl : l k) :
m / n * (k / l) = m * k / (n * l)
theorem nat.div_eq_self {m n : } :
m / n = m m = 0 n = 1
theorem nat.div_eq_sub_mod_div {m n : } :
m / n = (m - m % n) / n
theorem nat.not_dvd_of_between_consec_multiples {m n k : } (h1 : n * k < m) (h2 : m < n * (k + 1)) :
¬n m

m is not divisible by n if it is between n * k and n * (k + 1) for some k.

### find#

@[simp]
theorem nat.find_pos {p : Prop} (h : (n : ), p n) :
0 < ¬p 0
theorem nat.find_add {n : } {p : Prop} {hₘ : (m : ), p (m + n)} {hₙ : (n : ), p n} (hn : n nat.find hₙ) :
nat.find hₘ + n = nat.find hₙ

### find_greatest#

theorem nat.find_greatest_eq_iff {m k : } {P : Prop}  :
= m m k (m 0 P m) ⦃n : ⦄, m < n n k ¬P n
theorem nat.find_greatest_eq_zero_iff {k : } {P : Prop}  :
= 0 ⦃n : ⦄, 0 < n n k ¬P n
theorem nat.find_greatest_spec {m n : } {P : Prop} (hmb : m n) (hm : P m) :
P n)
theorem nat.find_greatest_le {P : Prop} (n : ) :
n
theorem nat.le_find_greatest {m n : } {P : Prop} (hmb : m n) (hm : P m) :
m
theorem nat.find_greatest_mono_right (P : Prop)  :
theorem nat.find_greatest_mono_left {P Q : Prop} (hPQ : P Q) :
theorem nat.find_greatest_mono {m n : } {P Q : Prop} (hPQ : P Q) (hmn : m n) :
theorem nat.find_greatest_is_greatest {n k : } {P : Prop} (hk : < k) (hkb : k n) :
¬P k
theorem nat.find_greatest_of_ne_zero {m n : } {P : Prop} (h : = m) (h0 : m 0) :
P m

### bit0 and bit1#

@[protected]
theorem nat.bit0_le {n m : } (h : n m) :
@[protected]
theorem nat.bit1_le {n m : } (h : n m) :
theorem nat.bit_le (b : bool) {m n : } :
m n m n
theorem nat.bit0_le_bit (b : bool) {m n : } :
m n bit0 m n
theorem nat.bit_le_bit1 (b : bool) {m n : } :
m n m bit1 n
theorem nat.bit_lt_bit0 (b : bool) {m n : } :
m < n m < bit0 n
theorem nat.bit_lt_bit {m n : } (a b : bool) (h : m < n) :
m < n
@[simp]
theorem nat.bit0_le_bit1_iff {m n : } :
bit0 m bit1 n m n
@[simp]
theorem nat.bit0_lt_bit1_iff {m n : } :
bit0 m < bit1 n m n
@[simp]
theorem nat.bit1_le_bit0_iff {m n : } :
bit1 m bit0 n m < n
@[simp]
theorem nat.bit1_lt_bit0_iff {m n : } :
bit1 m < bit0 n m < n
@[simp]
theorem nat.one_le_bit0_iff {n : } :
1 bit0 n 0 < n
@[simp]
theorem nat.one_lt_bit0_iff {n : } :
1 < bit0 n 1 n
@[simp]
theorem nat.bit_le_bit_iff {m n : } {b : bool} :
m n m n
@[simp]
theorem nat.bit_lt_bit_iff {m n : } {b : bool} :
m < n m < n
@[simp]
theorem nat.bit_le_bit1_iff {m n : } {b : bool} :
m bit1 n m n

### decidability of predicates #

@[protected, instance]
def nat.decidable_lo_hi (lo hi : ) (P : Prop) [H : decidable_pred P] :
decidable ( (x : ), lo x x < hi P x)
Equations
@[protected, instance]
def nat.decidable_lo_hi_le (lo hi : ) (P : Prop) [H : decidable_pred P] :
decidable ( (x : ), lo x x hi P x)
Equations