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.

TODO #

Move most of the theorems to Data.Nat.Defs by modifying their proofs.

instances #

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
  • 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 NeZero.one_le {n : } [NeZero n] :
1 n
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
@[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_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 : } :

sub #

Most lemmas come from the OrderedSub instance on .

theorem Nat.lt_pred_iff {m : } {n : } :
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 - Nat.succ n = 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 < Nat.succ m * 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.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 < 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, 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 Sk + 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 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.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.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.one_mod_of_ne_one {n : } :
n 11 % n = 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_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 : Prop} [DecidablePred p] (h : ∃ (n : ), p n) :
0 < Nat.find h ¬p 0
theorem Nat.find_add {n : } {p : Prop} [DecidablePred p] {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 : Prop} [DecidablePred P] :
Nat.findGreatest P k = m m k (m 0P m) ∀ ⦃n : ⦄, m < nn k¬P n
theorem Nat.findGreatest_eq_zero_iff {k : } {P : Prop} [DecidablePred P] :
Nat.findGreatest P k = 0 ∀ ⦃n : ⦄, 0 < nn k¬P n
@[simp]
theorem Nat.findGreatest_pos {k : } {P : Prop} [DecidablePred P] :
0 < Nat.findGreatest P k ∃ (n : ), 0 < n n k P n
theorem Nat.findGreatest_spec {m : } {n : } {P : Prop} [DecidablePred P] (hmb : m n) (hm : P m) :
theorem Nat.le_findGreatest {m : } {n : } {P : Prop} [DecidablePred P] (hmb : m n) (hm : P m) :
theorem Nat.findGreatest_mono {m : } {n : } {P : Prop} {Q : Prop} [DecidablePred P] [DecidablePred Q] (hPQ : P Q) (hmn : m n) :
theorem Nat.findGreatest_is_greatest {n : } {k : } {P : Prop} [DecidablePred P] (hk : Nat.findGreatest P n < k) (hkb : k n) :
¬P k
theorem Nat.findGreatest_of_ne_zero {m : } {n : } {P : Prop} [DecidablePred P] (h : Nat.findGreatest P n = 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 : Prop) [H : DecidablePred P] :
Decidable (∀ (x : ), lo xx < hiP x)
Equations
instance Nat.decidableLoHiLe (lo : ) (hi : ) (P : Prop) [DecidablePred P] :
Decidable (∀ (x : ), lo xx hiP x)
Equations