# Documentation

Mathlib.Data.Nat.Order.Basic

# The natural numbers as a linearly ordered commutative semiring #

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 #

instance Nat.orderBot :
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

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

Equations
Equations
Equations
Equations
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.

### Equalities and inequalities involving zero and one #

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 : } :
max 0 n = n
@[simp]
theorem Nat.min_eq_zero_iff {m : } {n : } :
min m n = 0 m = 0 n = 0
@[simp]
theorem Nat.max_eq_zero_iff {m : } {n : } :
max m n = 0 m = 0 n = 0
theorem Nat.add_eq_max_iff {m : } {n : } :
m + n = max m n m = 0 n = 0
theorem Nat.add_eq_min_iff {m : } {n : } :
m + n = min 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 : } :
n m

### sub#

Most lemmas come from the OrderedSub instance on ℕ.

Equations
theorem Nat.lt_pred_iff {m : } {n : } :
n < < 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 - = m - n - 1

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

### mul#

theorem Nat.mul_eq_one_iff {m : } {n : } :
m * n = 1 m = 1 n = 1
theorem Nat.succ_mul_pos {n : } (m : ) (hn : 0 < n) :
0 < * 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 < nm * 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

### 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 < bP (a + 1) bP a (b + 1)P (a + 1) (b + 1)) (a : ) (b : ) :
a < bP a b

Given a predicate on two naturals P : ℕ → ℕ → Prop→ ℕ → Prop→ 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 : } (hk : k S) (h_ind : ∀ (k : ), k Sk + 1 S) (hnk : k n) :
n S

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

theorem Nat.set_induction {S : } (hb : 0 S) (h_ind : ∀ (k : ), k Sk + 1 S) (n : ) :
n S

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

### div#

theorem Nat.div_le_of_le_mul' {m : } {n : } {k : } (h : m k * n) :
m / k n
theorem Nat.div_le_self' (m : ) (n : ) :
m / n m
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
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 = if k m % k + n % k then m % k + n % k - k else 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#

theorem Nat.find_pos {p : } [inst : ] (h : n, p n) :
0 < ¬p 0
theorem Nat.find_add {n : } {p : } [inst : ] {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.findGreatest_eq_iff {m : } {k : } {P : } [inst : ] :
= m m k (m 0P m) ∀ ⦃n : ⦄, m < nn k¬P n
theorem Nat.findGreatest_eq_zero_iff {k : } {P : } [inst : ] :
= 0 ∀ ⦃n : ⦄, 0 < nn k¬P n
theorem Nat.findGreatest_spec {m : } {n : } {P : } [inst : ] (hmb : m n) (hm : P m) :
P ()
theorem Nat.findGreatest_le {P : } [inst : ] (n : ) :
n
theorem Nat.le_findGreatest {m : } {n : } {P : } [inst : ] (hmb : m n) (hm : P m) :
m
theorem Nat.findGreatest_mono_right (P : ) [inst : ] :
theorem Nat.findGreatest_mono_left {P : } {Q : } [inst : ] [inst : ] (hPQ : P Q) :
theorem Nat.findGreatest_mono {m : } {n : } {P : } {Q : } [inst : ] [inst : ] (hPQ : P Q) (hmn : m n) :
theorem Nat.findGreatest_is_greatest {n : } {k : } {P : } [inst : ] (hk : < k) (hkb : k n) :
¬P k
theorem Nat.findGreatest_of_ne_zero {m : } {n : } {P : } [inst : ] (h : = m) (h0 : m 0) :
P m

### bit0 and bit1#

theorem Nat.bit0_le {n : } {m : } (h : n m) :
theorem Nat.bit1_le {n : } {m : } (h : n m) :
theorem Nat.bit_le (b : Bool) {m : } {n : } :
m nNat.bit b m Nat.bit b n
theorem Nat.bit0_le_bit (b : Bool) {m : } {n : } :
m nbit0 m Nat.bit b n
theorem Nat.bit_le_bit1 (b : Bool) {m : } {n : } :
m nNat.bit b m bit1 n
theorem Nat.bit_lt_bit0 (b : Bool) {m : } {n : } :
m < nNat.bit b m < bit0 n
theorem Nat.bit_lt_bit {m : } {n : } (a : Bool) (b : Bool) (h : m < n) :
Nat.bit a m < Nat.bit b 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

### decidability of predicates #

instance Nat.decidableLoHi (lo : ) (hi : ) (P : ) [H : ] :
Decidable ((x : ) → lo xx < hiP x)
Equations
instance Nat.decidableLoHiLe (lo : ) (hi : ) (P : ) [inst : ] :
Decidable ((x : ) → lo xx hiP x)
Equations