Documentation

Mathlib.Data.Nat.Init

Basic operations on the natural numbers #

This file contains:

This file should not depend on anything defined in Mathlib (except for notation), so that it can be upstreamed to Batteries or the Lean standard library easily.

See note [foundational algebra order theory].

succ, pred #

theorem Nat.succ_pos' {n : } :
0 < n.succ
theorem LT.lt.nat_succ_le {n m : } (h : n < m) :
n.succ m

Alias of Nat.succ_le_of_lt.

theorem Nat.of_le_succ {m n : } :
m n.succm n m = n.succ

Alias of the forward direction of Nat.le_succ_iff.

@[deprecated Nat.forall_lt_succ_right (since := "2025-08-21")]
theorem Nat.forall_lt_succ {n : } {p : Prop} :
(∀ (m : ), m < n + 1p m) (∀ (m : ), m < np m) p n

Alias of Nat.forall_lt_succ_right.


See forall_lt_succ_right' for a variant where p takes the bound as an argument.

@[deprecated Nat.exists_lt_succ_right (since := "2025-08-15")]
theorem Nat.exists_lt_succ {n : } {p : Prop} :
( (m : ), m < n + 1 p m) ( (m : ), m < n p m) p n

Alias of Nat.exists_lt_succ_right.


See exists_lt_succ_right' for a variant where p takes the bound as an argument.

theorem Nat.two_lt_of_ne {n : } :
n 0n 1n 22 < n
theorem Nat.two_le_iff (n : ) :
2 n n 0 n 1

add #

sub #

mul #

theorem Nat.mul_def {m n : } :
m.mul n = m * n
theorem Nat.two_mul_ne_two_mul_add_one {m n : } :
2 * n 2 * m + 1
@[deprecated Nat.mul_eq_left (since := "2025-06-05")]
theorem Nat.mul_right_eq_self_iff {a b : } (ha : a 0) :
a * b = a b = 1

Alias of Nat.mul_eq_left.

@[deprecated Nat.mul_eq_right (since := "2025-06-05")]
theorem Nat.mul_left_eq_self_iff {b a : } (hb : b 0) :
a * b = b a = 1

Alias of Nat.mul_eq_right.

@[deprecated Nat.eq_zero_of_two_mul_le (since := "2025-06-05")]
theorem Nat.eq_zero_of_double_le {n : } (h : 2 * n n) :
n = 0

Alias of Nat.eq_zero_of_two_mul_le.

div #

theorem Nat.le_div_two_iff_mul_two_le {n m : } :
m n / 2 m * 2 n
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.

@[deprecated Nat.sub_mul_div (since := "2025-04-15")]
theorem Nat.sub_mul_div' (a b c : ) :
(a - b * c) / b = a / b - c

Alias of Nat.sub_mul_div.

@[deprecated Nat.eq_zero_of_le_div_two (since := "2025-06-05")]
theorem Nat.eq_zero_of_le_half {n : } (h : n n / 2) :
n = 0

Alias of Nat.eq_zero_of_le_div_two.

@[deprecated Nat.le_div_two_of_div_two_lt_sub (since := "2025-06-05")]
theorem Nat.le_half_of_half_lt_sub {a b : } (h : a / 2 < a - b) :
b a / 2

Alias of Nat.le_div_two_of_div_two_lt_sub.

@[deprecated Nat.div_two_le_of_sub_le_div_two (since := "2025-06-05")]
theorem Nat.half_le_of_sub_le_half {a b : } (h : a - b a / 2) :
a / 2 b

Alias of Nat.div_two_le_of_sub_le_div_two.

@[deprecated Nat.div_le_of_le_mul (since := "2025-06-05")]
theorem Nat.div_le_of_le_mul' {m n k : } :
m k * nm / k n

Alias of Nat.div_le_of_le_mul.

@[deprecated Nat.div_le_self (since := "2025-06-05")]
theorem Nat.div_le_self' (n k : ) :
n / k n

Alias of Nat.div_le_self.

theorem Nat.two_mul_odd_div_two {n : } (hn : n % 2 = 1) :
2 * (n / 2) = n - 1

pow #

theorem Nat.one_le_pow' (n m : ) :
1 (m + 1) ^ n
theorem Nat.sq_sub_sq (a b : ) :
a ^ 2 - b ^ 2 = (a + b) * (a - b)

Alias of Nat.pow_two_sub_pow_two.

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)) :
rec h0 h 0 = h0
theorem Nat.rec_add_one {C : Sort u_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) (n : ) :
rec h0 h (n + 1) = h n (rec h0 h n)
@[simp]
theorem Nat.rec_one {C : Sort u_1} (h0 : C 0) (h : (n : ) → C nC (n + 1)) :
rec h0 h 1 = h 0 h0
def Nat.leRec {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) {m : } (h : n m) :
motive m h

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.

This is a version of Nat.le.rec that works for Sort u. Similarly to Nat.le.rec, it can be used as

induction hle using Nat.leRec with
| refl => sorry
| le_succ_of_le hle ih => sorry
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Nat.leRec_self {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) :
    leRec refl le_succ_of_le = refl
    @[simp]
    theorem Nat.leRec_succ {m n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) (h1 : n m) {h2 : n m + 1} :
    leRec refl le_succ_of_le h2 = le_succ_of_le h1 (leRec refl le_succ_of_le h1)
    theorem Nat.leRec_succ' {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) :
    leRec refl le_succ_of_le = le_succ_of_le refl
    theorem Nat.leRec_trans {n m k : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) (hnm : n m) (hmk : m k) :
    leRec refl le_succ_of_le = leRec (leRec refl (fun (x : ) (h : n x) => le_succ_of_le h) hnm) (fun (x : ) (h : m x) => le_succ_of_le ) hmk
    theorem Nat.leRec_succ_left {n : } {motive : (m : ) → n mSort u_1} (refl : motive n ) (le_succ_of_le : k : ⦄ → (h : n k) → motive k hmotive (k + 1) ) {m : } (h1 : n m) (h2 : n + 1 m) :
    leRec (le_succ_of_le refl) (fun (x : ) (h : n + 1 x) (ih : motive x ) => le_succ_of_le ih) h2 = leRec refl le_succ_of_le h1
    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.leRec.

    Equations
    Instances For
      theorem Nat.leRecOn_self {C : Sort u_1} {n : } {next : {k : } → C kC (k + 1)} (x : C n) :
      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) :
      leRecOn h2 next x = next (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) :
      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) :
      leRecOn next x = leRecOn hmk next (leRecOn hnm next x)
      theorem Nat.leRecOn_succ_left {C : Sort u_1} {n m : } {next : {k : } → C kC (k + 1)} (x : C n) (h1 : n m) (h2 : n + 1 m) :
      leRecOn h2 (fun {k : } => next) (next x) = leRecOn h1 (fun {k : } => next) x
      @[irreducible]
      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} :
          n.strongRecOn' h = h n fun (m : ) (x : m < n) => m.strongRecOn' 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. To use in an induction proof, the syntax is induction n, hn using Nat.le_induction (or the same for induction').

          This is an alias of Nat.leRec, specialized to Prop.

          def Nat.twoStepInduction {P : Sort u_1} (zero : P 0) (one : P 1) (more : (n : ) → P nP (n + 1)P (n + 2)) (a : ) :
          P a

          Induction principle deriving the next case from the two previous ones.

          Equations
          Instances For
            theorem Nat.strong_induction_on {p : Prop} (n : ) (h : ∀ (n : ), (∀ (m : ), m < np m)p n) :
            p n
            theorem Nat.case_strong_induction_on {p : Prop} (a : ) (hz : p 0) (hi : ∀ (n : ), (∀ (m : ), m np m)p (n + 1)) :
            p a
            def Nat.decreasingInduction {n : } {motive : (m : ) → m nSort u_1} (of_succ : (k : ) → (h : k < n) → motive (k + 1) hmotive k ) (self : motive n ) {m : } (mn : m n) :
            motive m mn

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

            For a version also assuming m ≤ k, see Nat.decreasingInduction'.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem Nat.decreasingInduction_self {n : } {motive : (m : ) → m nSort u_1} (of_succ : (k : ) → (h : k < n) → motive (k + 1) hmotive k ) (self : motive n ) :
              decreasingInduction of_succ self = self
              theorem Nat.decreasingInduction_succ {m n : } {motive : (m : ) → m n + 1Sort u_1} (of_succ : (k : ) → (h : k < n + 1) → motive (k + 1) hmotive k ) (self : motive (n + 1) ) (mn : m n) (msn : m n + 1) :
              decreasingInduction of_succ self msn = decreasingInduction (fun (x : ) (x_1 : x < n) => of_succ x ) (of_succ n self) mn
              @[simp]
              theorem Nat.decreasingInduction_succ' {n : } {motive : (m : ) → m n + 1Sort u_1} (of_succ : (k : ) → (h : k < n + 1) → motive (k + 1) hmotive k ) (self : motive (n + 1) ) :
              decreasingInduction of_succ self = of_succ n self
              theorem Nat.decreasingInduction_trans {m n k : } {motive : (m : ) → m kSort u_1} (hmn : m n) (hnk : n k) (of_succ : (k_1 : ) → (h : k_1 < k) → motive (k_1 + 1) hmotive k_1 ) (self : motive k ) :
              decreasingInduction of_succ self = decreasingInduction (fun (x : ) (x_1 : x < n) => of_succ x ) (decreasingInduction of_succ self hnk) hmn
              theorem Nat.decreasingInduction_succ_left {m n : } {motive : (m : ) → m nSort u_1} (of_succ : (k : ) → (h : k < n) → motive (k + 1) hmotive k ) (self : motive n ) (smn : m + 1 n) (mn : m n) :
              decreasingInduction of_succ self mn = of_succ m smn (decreasingInduction of_succ self smn)
              @[irreducible]
              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
                @[irreducible]
                def Nat.pincerRecursion {P : Sort u_1} (Ha0 : (m : ) → P m 0) (H0b : (n : ) → P 0 n) (H : (x y : ) → P x y.succP x.succ yP x.succ y.succ) (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' {m n : } {P : Sort u_1} (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 Nat.decreasingInduction.

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

                    mod, dvd #

                    theorem Nat.not_pos_pow_dvd {a n : } (ha : 1 < a) (hn : 1 < n) :
                    ¬a ^ n a
                    @[deprecated Nat.not_dvd_of_lt_of_lt_mul_succ (since := "2025-06-05")]
                    theorem Nat.not_dvd_of_between_consec_multiples {n k m : } (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.

                    @[simp]
                    theorem Nat.not_two_dvd_bit1 (n : ) :
                    ¬2 2 * n + 1
                    @[simp]
                    theorem Nat.dvd_add_self_left {m n : } :
                    m m + n m n

                    A natural number m divides the sum m + n if and only if m divides n.

                    @[simp]
                    theorem Nat.dvd_add_self_right {m n : } :
                    m n + m m n

                    A natural number m divides the sum n + m if and only if m divides n.

                    @[deprecated Nat.not_dvd_iff_lt_mul_succ (since := "2025-06-05")]
                    theorem Nat.not_dvd_iff_between_consec_multiples (n : ) {a : } (ha : 0 < a) :
                    ¬a n (k : ), a * k < n n < a * (k + 1)

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

                    theorem Nat.dvd_right_iff_eq {m n : } :
                    (∀ (a : ), m a n a) m = n

                    Two natural numbers are equal if and only if they have the same multiples.

                    theorem Nat.dvd_left_iff_eq {m n : } :
                    (∀ (a : ), a m a n) m = n

                    Two natural numbers are equal if and only if they have the same divisors.

                    Decidability of predicates #

                    instance Nat.decidableLoHi (lo hi : ) (P : Prop) [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

                    Nat.AtLeastTwo #

                    class Nat.AtLeastTwo (n : ) :

                    A type class for natural numbers which are greater than or equal to 2.

                    NeZero and AtLeastTwo are used for numeric literals, and also for groups of related lemmas sharing a common value of n that needs to be nonzero, or at least 2, and where it is convenient to pass this information implicitly. Instances for these classes cover some of the cases where it is most structurally obvious from the syntactic form of n that it satisfies the required conditions, such as m + 1. Less widely used cases may be defined as lemmas rather than global instances and then made into instances locally where needed. If implicit arguments, appearing before other explicit arguments, are allowed to be autoParams in a future version of Lean, such an autoParam that is proved by cutsat might be a more general replacement for the use of typeclass inference for this purpose.

                    Instances
                      @[instance 100]