Documentation

Mathlib.Data.Nat.Defs

Basic operations on the natural numbers #

This file contains:

Implementation note #

Std has a home-baked development of the algebraic and order theoretic theory of which, in particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness libraries in mathlib (naturals show up as indices in lists, cardinality in finsets, powers in groups, ...). This home-baked development is pursued in this file.

Less basic uses of should however use the typeclass-mediated development. Data.Nat.Basic gives access to the algebraic instances. Data.Nat.Order.Basic is the one giving access to the algebraic order instances.

TODO #

The names of this file, Data.Nat.Basic and Data.Nat.Order.Basic are archaic and don't match up with reality anymore. Rename them.

succ, pred #

theorem Nat.succ_pos' {n : } :
theorem Nat.succ_inj {a : } {b : } :

Alias of Nat.succ_inj'.

theorem Nat.succ_ne_succ {m : } {n : } :
@[simp]
theorem LT.lt.nat_succ_le {n : } {m : } (h : n < m) :

Alias of Nat.succ_le_of_lt.

theorem Nat.succ_le_iff {m : } {n : } :
Nat.succ m n m < n
theorem Nat.le_succ_iff {m : } {n : } :
theorem Nat.of_le_succ {m : } {n : } :
m Nat.succ nm n m = Nat.succ n

Alias of the forward direction of Nat.le_succ_iff.

theorem Nat.lt_iff_le_pred {m : } {n : } :
0 < n(m < n m n - 1)
theorem Nat.le_of_pred_lt {n : } {m : } :
Nat.pred m < nm n
theorem Nat.lt_iff_add_one_le {m : } {n : } :
m < n m + 1 n
theorem Nat.lt_add_one_iff {m : } {n : } :
m < n + 1 m n
theorem Nat.lt_one_add_iff {m : } {n : } :
m < 1 + n m n
theorem Nat.add_one_le_iff {m : } {n : } :
m + 1 n m < n
theorem Nat.one_add_le_iff {m : } {n : } :
1 + m n m < n
theorem Nat.one_le_iff_ne_zero {n : } :
1 n n 0
@[simp]
theorem Nat.lt_one_iff {n : } :
n < 1 n = 0
theorem Nat.one_le_of_lt {a : } {b : } (h : a < b) :
1 b
@[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
@[simp]
theorem Nat.pred_one_add (n : ) :
Nat.pred (1 + n) = n

This ensures that simp succeeds on pred (n + 1) = n.

theorem Nat.pred_eq_self_iff {n : } :
Nat.pred n = n n = 0
theorem Nat.pred_eq_of_eq_succ {m : } {n : } (H : m = Nat.succ n) :
@[simp]
theorem Nat.pred_eq_succ_iff {m : } {n : } :
Nat.pred n = Nat.succ m n = m + 2
theorem Nat.and_forall_succ {p : Prop} :
(p 0 ∀ (n : ), p (n + 1)) ∀ (n : ), p n
theorem Nat.or_exists_succ {p : Prop} :
(p 0 ∃ (n : ), p (n + 1)) ∃ (n : ), p n
theorem Nat.forall_lt_succ {n : } {p : Prop} :
(∀ (m : ), m < n + 1p m) (∀ (m : ), m < np m) p n
theorem Nat.exists_lt_succ {n : } {p : Prop} :
(∃ (m : ), m < n + 1 p m) (∃ (m : ), m < n p m) p n
theorem Nat.two_lt_of_ne {n : } :
n 0n 1n 22 < n

pred #

@[simp]
theorem Nat.add_succ_sub_one (m : ) (n : ) :
m + Nat.succ n - 1 = m + n
@[simp]
theorem Nat.succ_add_sub_one (n : ) (m : ) :
Nat.succ m + n - 1 = m + n
theorem Nat.pred_sub (n : ) (m : ) :
Nat.pred n - m = Nat.pred (n - m)
theorem Nat.self_add_sub_one (n : ) :
n + (n - 1) = 2 * n - 1
theorem Nat.sub_one_add_self (n : ) :
n - 1 + n = 2 * n - 1
theorem Nat.self_add_pred (n : ) :
n + Nat.pred n = Nat.pred (2 * n)
theorem Nat.pred_add_self (n : ) :
Nat.pred n + n = Nat.pred (2 * n)
theorem Nat.pred_le_iff {m : } {n : } :
theorem Nat.lt_of_lt_pred {m : } {n : } (h : m < n - 1) :
m < n
theorem Nat.le_add_pred_of_pos {b : } (a : ) (hb : b 0) :
a b + (a - 1)

add #

@[simp]
theorem Nat.add_left_inj {m : } {k : } {n : } :
m + n = k + n m = k

Alias of Nat.add_right_cancel_iff.

@[simp]
theorem Nat.add_right_inj {m : } {k : } {n : } :
n + m = n + k m = k

Alias of Nat.add_left_cancel_iff.

@[simp]
theorem Nat.add_def {m : } {n : } :
Nat.add m n = m + n
theorem Nat.two_le_iff (n : ) :
2 n n 0 n 1
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
@[simp]
theorem Nat.add_eq_zero {m : } {n : } :
m + n = 0 m = 0 n = 0
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 {a : } {b : } {c : } {d : } (hab : a < b) (hcd : c < d) :
a + c + 1 < b + d
theorem Nat.le_or_le_of_add_eq_add_pred {a : } {b : } {c : } {d : } (h : a + c = b + d - 1) :
b a d c

sub #

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 _.

theorem Nat.lt_sub_iff_add_lt {a : } {b : } {c : } :
a < c - b a + b < c
theorem Nat.lt_sub_iff_add_lt' {a : } {b : } {c : } :
a < c - b b + a < c
theorem Nat.sub_lt_iff_lt_add {a : } {b : } {c : } (hba : b a) :
a - b < c a < b + c
theorem Nat.sub_lt_iff_lt_add' {a : } {b : } {c : } (hba : b a) :
a - b < c a < c + b
theorem Nat.sub_sub_sub_cancel_right {a : } {b : } {c : } (h : c b) :
a - c - (b - c) = a - b
theorem Nat.add_sub_sub_cancel {a : } {b : } {c : } (h : c a) :
a + b - (a - c) = b + c
theorem Nat.sub_add_sub_cancel {a : } {b : } {c : } (hab : b a) (hcb : c b) :
a - b + (b - c) = a - c
theorem Nat.lt_pred_iff {a : } {b : } :
theorem Nat.sub_lt_sub_iff_right {a : } {b : } {c : } (h : c a) :
a - c < b - c a < b

mul #

@[simp]
theorem Nat.mul_def {m : } {n : } :
Nat.mul m n = m * n
theorem Nat.zero_eq_mul {m : } {n : } :
0 = m * n m = 0 n = 0
theorem Nat.two_mul_ne_two_mul_add_one {m : } {n : } :
2 * n 2 * m + 1
theorem Nat.mul_left_inj {a : } {b : } {c : } (ha : a 0) :
b * a = c * a b = c
theorem Nat.mul_right_inj {a : } {b : } {c : } (ha : a 0) :
a * b = a * c b = c
theorem Nat.mul_ne_mul_left {a : } {b : } {c : } (ha : a 0) :
b * a c * a b c
theorem Nat.mul_ne_mul_right {a : } {b : } {c : } (ha : a 0) :
a * b a * c b c
theorem Nat.mul_eq_left {a : } {b : } (ha : a 0) :
a * b = a b = 1
theorem Nat.mul_eq_right {a : } {b : } (hb : b 0) :
a * b = b a = 1
theorem Nat.mul_right_eq_self_iff {a : } {b : } (ha : 0 < a) :
a * b = a b = 1
theorem Nat.mul_left_eq_self_iff {a : } {b : } (hb : 0 < b) :
a * b = b a = 1
theorem Nat.le_of_mul_le_mul_right {a : } {b : } {c : } (h : a * c b * c) (hc : 0 < c) :
a b
theorem Nat.one_lt_mul_iff {m : } {n : } :
1 < m * n 0 < m 0 < n (1 < m 1 < n)

The product of two natural numbers is greater than 1 if and only if at least one of them is greater than 1 and both are positive.

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
@[simp]
theorem Nat.lt_mul_iff_one_lt_left {a : } {b : } (hb : 0 < b) :
b < a * b 1 < a
@[simp]
theorem Nat.lt_mul_iff_one_lt_right {a : } {b : } (ha : 0 < a) :
a < a * b 1 < b
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.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_lt_mul'' {a : } {b : } {c : } {d : } (hac : a < c) (hbd : b < d) :
a * b < c * d
theorem Nat.mul_self_lt_mul_self {m : } {n : } (h : m < n) :
m * m < n * n
theorem Nat.mul_self_le_mul_self_iff {m : } {n : } :
m * m n * n m n
theorem Nat.mul_self_lt_mul_self_iff {m : } {n : } :
m * m < n * n m < n
theorem Nat.le_mul_self (n : ) :
n n * n
theorem Nat.mul_self_inj {m : } {n : } :
m * m = n * n m = n
@[simp]
theorem Nat.lt_mul_self_iff {n : } :
n < n * n 1 < n
theorem Nat.add_sub_one_le_mul {a : } {b : } (ha : a 0) (hb : b 0) :
a + b - 1 a * b
theorem Nat.add_le_mul {a : } (ha : 2 a) {b : } :
2 ba + b a * b

div #

theorem Nat.div_le_iff_le_mul_add_pred {a : } {b : } {c : } (hb : 0 < b) :
a / b c a b * c + (b - 1)
theorem Nat.div_lt_self' (a : ) (b : ) :
(a + 1) / (b + 2) < a + 1

A version of Nat.div_lt_self using successors, rather than additional hypotheses.

theorem Nat.le_div_iff_mul_le' {a : } {b : } {c : } (hb : 0 < b) :
a c / b a * b c
theorem Nat.div_lt_iff_lt_mul' {a : } {b : } {c : } (hb : 0 < b) :
a / b < c a < c * b
theorem Nat.one_le_div_iff {a : } {b : } (hb : 0 < b) :
1 a / b b a
theorem Nat.div_lt_one_iff {a : } {b : } (hb : 0 < b) :
a / b < 1 a < b
theorem Nat.div_le_div_right {a : } {b : } {c : } (h : a b) :
a / c b / c
theorem Nat.lt_of_div_lt_div {a : } {b : } {c : } (h : a / c < b / c) :
a < b
theorem Nat.div_pos {a : } {b : } (hba : b a) (hb : 0 < b) :
0 < a / b
theorem Nat.lt_mul_of_div_lt {a : } {b : } {c : } (h : a / c < b) (hc : 0 < c) :
a < b * c
theorem Nat.mul_div_le_mul_div_assoc (a : ) (b : ) (c : ) :
a * (b / c) a * b / c
theorem Nat.eq_mul_of_div_eq_left {a : } {b : } {c : } (H1 : b a) (H2 : a / b = c) :
a = c * b
theorem Nat.mul_div_cancel_left' {a : } {b : } (Hd : a b) :
a * (b / a) = b
theorem Nat.lt_div_mul_add {a : } {b : } (hb : 0 < b) :
a < a / b * b + b
@[simp]
theorem Nat.div_left_inj {a : } {b : } {d : } (hda : d a) (hdb : d b) :
a / d = b / d a = b
theorem Nat.div_mul_div_comm {a : } {b : } {c : } {d : } :
b ad ca / b * (c / d) = a * c / (b * d)
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 (a : ) (b : ) (c : ) :
a / c * b / a b / c
theorem Nat.eq_zero_of_le_half {n : } (h : n n / 2) :
n = 0
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
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.two_mul_odd_div_two {n : } (hn : n % 2 = 1) :
2 * (n / 2) = n - 1
theorem Nat.div_le_div_left {a : } {b : } {c : } (hcb : c b) (hc : 0 < c) :
a / b a / c
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.eq_div_of_mul_eq_left {a : } {b : } {c : } (hc : c 0) (h : a * c = b) :
a = b / c
theorem Nat.eq_div_of_mul_eq_right {a : } {b : } {c : } (hc : c 0) (h : c * a = b) :
a = b / c

pow #

TODO #

theorem Nat.pow_lt_pow_left {a : } {b : } (h : a < b) {n : } :
n 0a ^ n < b ^ n
theorem Nat.pow_lt_pow_right {a : } {m : } {n : } (ha : 1 < a) (h : m < n) :
a ^ m < a ^ n
theorem Nat.pow_le_pow_iff_left {a : } {b : } {n : } (hn : n 0) :
a ^ n b ^ n a b
theorem Nat.pow_lt_pow_iff_left {a : } {b : } {n : } (hn : n 0) :
a ^ n < b ^ n a < b
theorem Nat.pow_left_injective {n : } (hn : n 0) :
Function.Injective fun (a : ) => a ^ n
theorem Nat.pow_right_injective {a : } (ha : 2 a) :
Function.Injective fun (x : ) => a ^ x
@[simp]
theorem Nat.pow_eq_zero {a : } {n : } :
a ^ n = 0 a = 0 n 0
theorem Nat.le_self_pow {n : } (hn : n 0) (a : ) :
a a ^ n
theorem Nat.lt_pow_self {a : } (ha : 1 < a) (n : ) :
n < a ^ n
theorem Nat.lt_two_pow (n : ) :
n < 2 ^ n
theorem Nat.one_le_pow (n : ) (m : ) (h : 0 < m) :
1 m ^ n
theorem Nat.one_le_pow' (n : ) (m : ) :
1 (m + 1) ^ n
theorem Nat.one_lt_pow {a : } {n : } (hn : n 0) (ha : 1 < a) :
1 < a ^ n
theorem Nat.two_pow_succ (n : ) :
2 ^ (n + 1) = 2 ^ n + 2 ^ n
theorem Nat.one_lt_pow' (n : ) (m : ) :
1 < (m + 2) ^ (n + 1)
@[simp]
theorem Nat.one_lt_pow_iff {n : } (hn : n 0) {a : } :
1 < a ^ n 1 < a
theorem Nat.one_lt_two_pow' (n : ) :
1 < 2 ^ (n + 1)
theorem Nat.mul_lt_mul_pow_succ {a : } {b : } {n : } (ha : 0 < a) (hb : 1 < b) :
n * b < a * b ^ (n + 1)
theorem Nat.sq_sub_sq (a : ) (b : ) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)
theorem Nat.pow_two_sub_pow_two (a : ) (b : ) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)

Alias of Nat.sq_sub_sq.

theorem Nat.div_pow {a : } {b : } {c : } (h : a b) :
(b / a) ^ c = b ^ c / a ^ c

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.

@[simp]
theorem Nat.rec_zero {C : Sort u_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) :
Nat.rec h0 h 0 = h0
@[simp]
theorem Nat.rec_add_one {C : Sort u_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) (n : ) :
Nat.rec h0 h (n + 1) = h n (Nat.rec h0 h n)
def Nat.leRecOn' {n : } {C : Sort u_1} {m : } :
n m(k : ⦄ → n kC kC (k + 1))C nC m

Recursion starting at a non-zero number: given a map C k → C (k+1) for each k ≥ n, there is a map from C n to each C m, n ≤ m.

Equations
Instances For
    def Nat.leRecOn {C : Sort u_1} {n : } {m : } :
    n m({k : } → C kC (k + 1))C nC m

    Recursion starting at a non-zero number: given a map C k → C (k + 1) for each k, there is a map from C n to each C m, n ≤ m. For a version where the assumption is only made when k ≥ n, see Nat.leRecOn'.

    Equations
    Instances For
      theorem Nat.leRecOn_self {C : Sort u_1} {n : } {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn (fun {k : } => next) x = x
      theorem Nat.leRecOn_succ {C : Sort u_1} {n : } {m : } (h1 : n m) {h2 : n m + 1} {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn h2 next x = next (Nat.leRecOn h1 (fun {k : } => next) x)
      theorem Nat.leRecOn_succ' {C : Sort u_1} {n : } {h : n n + 1} {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn h (fun {k : } => next) x = next x
      theorem Nat.leRecOn_trans {C : Sort u_1} {n : } {m : } {k : } (hnm : n m) (hmk : m k) {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn next x = Nat.leRecOn hmk next (Nat.leRecOn hnm next x)
      theorem Nat.leRecOn_succ_left {C : Sort u_1} {n : } {m : } (h1 : n m) (h2 : n + 1 m) {next : {k : } → C kC (k + 1)} (x : C n) :
      Nat.leRecOn h2 (fun {k : } => next) (next x) = Nat.leRecOn h1 (fun {k : } => next) x
      theorem Nat.leRecOn_injective {C : Sort u_1} {n : } {m : } (hnm : n m) (next : {k : } → C kC (k + 1)) (Hnext : ∀ (n : ), Function.Injective next) :
      Function.Injective (Nat.leRecOn hnm fun {k : } => next)
      theorem Nat.leRecOn_surjective {C : Sort u_1} {n : } {m : } (hnm : n m) (next : {k : } → C kC (k + 1)) (Hnext : ∀ (n : ), Function.Surjective next) :
      Function.Surjective (Nat.leRecOn hnm fun {k : } => next)
      def Nat.strongRec' {p : Sort u_1} (H : (n : ) → ((m : ) → m < np m)p n) (n : ) :
      p n

      Recursion principle based on <.

      Equations
      Instances For
        def Nat.strongRecOn' {P : Sort u_1} (n : ) (h : (n : ) → ((m : ) → m < nP m)P n) :
        P n

        Recursion principle based on < applied to some natural number.

        Equations
        Instances For
          theorem Nat.strongRecOn'_beta {n : } {P : Sort u_1} {h : (n : ) → ((m : ) → m < nP m)P n} :
          Nat.strongRecOn' n h = h n fun (m : ) (x : m < n) => Nat.strongRecOn' m h
          theorem Nat.le_induction {m : } {P : (n : ) → m nProp} (base : P m ) (succ : ∀ (n : ) (hmn : m n), P n hmnP (n + 1) ) (n : ) (hmn : m n) :
          P n hmn

          Induction principle starting at a non-zero number. For maps to a Sort* see leRecOn. To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction').

          def Nat.decreasingInduction {m : } {n : } {P : Sort u_1} (h : (n : ) → P (n + 1)P n) (mn : m n) (hP : P n) :
          P m

          Decreasing induction: if P (k+1) implies P k, then P n implies P m for all m ≤ n. Also works for functions to Sort*. For m version assuming only the assumption for k < n, see decreasing_induction'.

          Equations
          Instances For
            @[simp]
            theorem Nat.decreasingInduction_self {n : } {P : Sort u_1} (h : (n : ) → P (n + 1)P n) (nn : n n) (hP : P n) :
            theorem Nat.decreasingInduction_succ {m : } {n : } {P : Sort u_1} (h : (n : ) → P (n + 1)P n) (mn : m n) (msn : m n + 1) (hP : P (n + 1)) :
            @[simp]
            theorem Nat.decreasingInduction_succ' {P : Sort u_1} (h : (n : ) → P (n + 1)P n) {m : } (msm : m m + 1) (hP : P (m + 1)) :
            Nat.decreasingInduction h msm hP = h m hP
            theorem Nat.decreasingInduction_trans {m : } {n : } {k : } {P : Sort u_1} (h : (n : ) → P (n + 1)P n) (hmn : m n) (hnk : n k) (hP : P k) :
            theorem Nat.decreasingInduction_succ_left {m : } {n : } {P : Sort u_1} (h : (n : ) → P (n + 1)P n) (smn : m + 1 n) (mn : m n) (hP : P n) :
            def Nat.strongSubRecursion {P : Sort u_1} (H : (m n : ) → ((x y : ) → x < my < nP x y)P m n) (n : ) (m : ) :
            P n m

            Given P : ℕ → ℕ → Sort*, if for all m n : ℕ we can extend P from the rectangle strictly below (m, n) to P m n, then we have P n m for all n m : ℕ. Note that for non-Prop output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas.

            Equations
            Instances For
              def Nat.pincerRecursion {P : Sort u_1} (Ha0 : (m : ) → P m 0) (H0b : (n : ) → P 0 n) (H : (x y : ) → P x (Nat.succ y)P (Nat.succ x) yP (Nat.succ x) (Nat.succ y)) (n : ) (m : ) :
              P n m

              Given P : ℕ → ℕ → Sort*, if we have P m 0 and P 0 n for all m n : ℕ, and for any m n : ℕ we can extend P from (m, n + 1) and (m + 1, n) to (m + 1, n + 1) then we have P m n for all m n : ℕ.

              Note that for non-Prop output it is preferable to use the equation compiler directly if possible, since this produces equation lemmas.

              Equations
              Instances For
                def Nat.decreasingInduction' {P : Sort u_1} {m : } {n : } (h : (k : ) → k < nm kP (k + 1)P k) (mn : m n) (hP : P n) :
                P m

                Decreasing induction: if P (k+1) implies P k for all m ≤ k < n, then P n implies P m. Also works for functions to Sort*. Weakens the assumptions of decreasing_induction.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  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 .

                  mod, dvd #

                  theorem Nat.mul_div_mul_comm_of_dvd_dvd {a : } {b : } {c : } {d : } (hba : b a) (hdc : d c) :
                  a * c / (b * d) = a / b * (c / d)
                  @[simp]
                  theorem Nat.mul_mod_mod (a : ) (b : ) (c : ) :
                  a * (b % c) % c = a * b % c
                  @[simp]
                  theorem Nat.mod_mul_mod (a : ) (b : ) (c : ) :
                  a % c * b % c = a * b % c
                  theorem Nat.pow_mod (a : ) (b : ) (n : ) :
                  a ^ b % n = (a % n) ^ b % n
                  theorem Nat.not_pos_pow_dvd {a : } {n : } :
                  1 < a1 < n¬a ^ n a
                  theorem Nat.lt_of_pow_dvd_right {a : } {b : } {n : } (hb : b 0) (ha : 2 a) (h : a ^ n b) :
                  n < b
                  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.mod_eq_iff_lt {m : } {n : } (hn : n 0) :
                  m % n = m m < n
                  @[simp]
                  theorem Nat.mod_succ_eq_iff_lt {m : } {n : } :
                  m % Nat.succ n = m m < Nat.succ n
                  @[simp]
                  theorem Nat.mod_succ (n : ) :
                  n % Nat.succ n = n
                  theorem Nat.mod_add_div' (a : ) (b : ) :
                  a % b + a / b * b = a
                  theorem Nat.div_add_mod' (a : ) (b : ) :
                  a / b * b + a % b = a
                  theorem Nat.div_mod_unique {a : } {b : } {c : } {d : } (h : 0 < b) :
                  a / b = d a % b = c c + b * d = a c < b

                  See also Nat.divModEquiv for a similar statement as an Equiv.

                  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.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.

                  theorem Nat.dvd_add_left {a : } {b : } {c : } (h : a c) :
                  a b + c a b
                  theorem Nat.dvd_add_right {a : } {b : } {c : } (h : a b) :
                  a b + c a c
                  theorem Nat.mul_dvd_mul_iff_left {a : } {b : } {c : } (ha : 0 < a) :
                  a * b a * c b c
                  theorem Nat.mul_dvd_mul_iff_right {a : } {b : } {c : } (hc : 0 < c) :
                  a * c b * c a b
                  theorem Nat.add_mod_eq_add_mod_right {a : } {b : } {d : } (c : ) (H : a % d = b % d) :
                  (a + c) % d = (b + c) % d
                  theorem Nat.add_mod_eq_add_mod_left {a : } {b : } {d : } (c : ) (H : a % d = b % d) :
                  (c + a) % d = (c + b) % d
                  theorem Nat.mul_dvd_of_dvd_div {a : } {b : } {c : } (hcb : c b) (h : a b / c) :
                  c * a b
                  theorem Nat.eq_of_dvd_of_div_eq_one {a : } {b : } (hab : a b) (h : b / a = 1) :
                  a = b
                  theorem Nat.eq_zero_of_dvd_of_div_eq_zero {a : } {b : } (hab : a b) (h : b / a = 0) :
                  b = 0
                  theorem Nat.div_le_div {a : } {b : } {c : } {d : } (h1 : a b) (h2 : d c) (h3 : d 0) :
                  a / c b / d
                  theorem Nat.lt_mul_div_succ {b : } (a : ) (hb : 0 < b) :
                  a < b * (a / b + 1)
                  theorem Nat.mul_add_mod' (a : ) (b : ) (c : ) :
                  (a * b + c) % b = c % b
                  theorem Nat.mul_add_mod_of_lt {a : } {b : } {c : } (h : c < b) :
                  (a * b + c) % b = c

                  find #

                  theorem Nat.find_eq_iff {m : } {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) :
                  Nat.find h = m p m ∀ (n : ), n < m¬p n
                  @[simp]
                  theorem Nat.find_lt_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
                  Nat.find h < n ∃ (m : ), m < n p m
                  @[simp]
                  theorem Nat.find_le_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
                  Nat.find h n ∃ (m : ), m n p m
                  @[simp]
                  theorem Nat.le_find_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
                  n Nat.find h ∀ (m : ), m < n¬p m
                  @[simp]
                  theorem Nat.lt_find_iff {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) (n : ) :
                  n < Nat.find h ∀ (m : ), m n¬p m
                  @[simp]
                  theorem Nat.find_eq_zero {p : Prop} [DecidablePred p] (h : ∃ (n : ), p n) :
                  Nat.find h = 0 p 0
                  theorem Nat.find_mono {p : Prop} {q : Prop} [DecidablePred p] [DecidablePred q] (h : ∀ (n : ), q np n) {hp : ∃ (n : ), p n} {hq : ∃ (n : ), q n} :
                  theorem Nat.find_le {n : } {p : Prop} [DecidablePred p] {h : ∃ (n : ), p n} (hn : p n) :
                  theorem Nat.find_comp_succ {p : Prop} [DecidablePred p] (h₁ : ∃ (n : ), p n) (h₂ : ∃ (n : ), p (n + 1)) (h0 : ¬p 0) :
                  Nat.find h₁ = Nat.find h₂ + 1
                  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ₙ

                  Nat.findGreatest #

                  def Nat.findGreatest (P : Prop) [DecidablePred P] :

                  Nat.findGreatest P n is the largest i ≤ bound such that P i holds, or 0 if no such i exists

                  Equations
                  Instances For
                    theorem Nat.findGreatest_succ {P : Prop} [DecidablePred P] (n : ) :
                    Nat.findGreatest P (n + 1) = if P (n + 1) then n + 1 else Nat.findGreatest P n
                    @[simp]
                    theorem Nat.findGreatest_eq {P : Prop} [DecidablePred P] {n : } :
                    P nNat.findGreatest P n = n
                    @[simp]
                    theorem Nat.findGreatest_of_not {P : Prop} [DecidablePred P] {n : } (h : ¬P (n + 1)) :
                    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 : } {P : Prop} [DecidablePred P] {n : } (hmb : m n) (hm : P m) :
                    theorem Nat.le_findGreatest {m : } {P : Prop} [DecidablePred P] {n : } (hmb : m n) (hm : P m) :
                    theorem Nat.findGreatest_mono_left {P : Prop} {Q : Prop} [DecidablePred P] [DecidablePred Q] (hPQ : ∀ (n : ), P nQ n) (n : ) :
                    theorem Nat.findGreatest_mono {m : } {P : Prop} {Q : Prop} [DecidablePred P] {n : } [DecidablePred Q] (hPQ : ∀ (n : ), P nQ n) (hmn : m n) :
                    theorem Nat.findGreatest_is_greatest {k : } {P : Prop} [DecidablePred P] {n : } (hk : Nat.findGreatest P n < k) (hkb : k n) :
                    ¬P k
                    theorem Nat.findGreatest_of_ne_zero {m : } {P : Prop} [DecidablePred P] {n : } (h : Nat.findGreatest P n = m) (h0 : m 0) :
                    P m

                    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