Basic operations on the natural numbers #

This file contains:

some basic lemmas about natural numbers
extra recursors:
- leRecOn, le_induction: recursion and induction principles starting at non-zero numbers
- decreasing_induction: recursion growing downwards
- le_rec_on', decreasing_induction': versions with slightly weaker assumptions
- strong_rec': recursion based on strong inequalities
decidability instances on predicates about the natural numbers

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

source

def Mathlib.LibraryNote.«foundational algebra order theory» :

LibraryNote

Batteries has a home-baked development of the algebraic and order-theoretic theory of ℕ and `ℤ which, in particular, is not typeclass-mediated. This is useful to set up the algebra and finiteness libraries in mathlib (naturals and integers show up as indices/offsets in lists, cardinality in finsets, powers in groups, ...).

Less basic uses of ℕ and ℤ should however use the typeclass-mediated development.

The relevant files are:

Mathlib/Data/Nat/Basic.lean for the continuation of the home-baked development on ℕ
Mathlib/Data/Int/Init.lean for the continuation of the home-baked development on ℤ
Mathlib/Algebra/Group/Nat.lean for the monoid instances on ℕ
Mathlib/Algebra/Group/Int.lean for the group instance on ℤ
Mathlib/Algebra/Ring/Nat.lean for the semiring instance on ℕ
Mathlib/Algebra/Ring/Int.lean for the ring instance on ℤ
Mathlib/Algebra/Order/Group/Nat.lean for the ordered monoid instance on ℕ
Mathlib/Algebra/Order/Group/Int.lean for the ordered group instance on ℤ
Mathlib/Algebra/Order/Ring/Nat.lean for the ordered semiring instance on ℕ
Mathlib/Algebra/Order/Ring/Int.lean for the ordered ring instance on ℤ

Equations

Mathlib.LibraryNote.«foundational algebra order theory» = ()

Instances For

`succ`, `pred` #

source

theorem Nat.succ_pos' {n : ℕ} :

0 < n.succ

source

theorem LT.lt.nat_succ_le {n m : ℕ} (h : n < m) :

n.succ ≤ m

Alias of Nat.succ_le_of_lt.

source

theorem Nat.of_le_succ {m n : ℕ} :

m ≤ n.succ → m ≤ n ∨ m = n.succ

Alias of the forward direction of Nat.le_succ_iff.

source

@[deprecated Nat.forall_lt_succ_right (since := "2025-08-21")]

theorem Nat.forall_lt_succ {n : ℕ} {p : ℕ → Prop} :

(∀ (m : ℕ), m < n + 1 → p m) ↔ (∀ (m : ℕ), m < n → p 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.

source

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

source

theorem Nat.two_lt_of_ne {n : ℕ} :

n ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < n

source

theorem Nat.two_le_iff (n : ℕ) :

2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1

`add` #

`sub` #

`mul` #

source

theorem Nat.mul_def {m n : ℕ} :

m.mul n = m * n

source

theorem Nat.two_mul_ne_two_mul_add_one {m n : ℕ} :

2 * n ≠ 2 * m + 1

source

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

source

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

source

@[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` #

source

theorem Nat.le_div_two_iff_mul_two_le {n m : ℕ} :

m ≤ n / 2 ↔ ↑m * 2 ≤ ↑n

source

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.

source

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

source

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

source

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

source

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

source

@[deprecated Nat.div_le_of_le_mul (since := "2025-06-05")]

theorem Nat.div_le_of_le_mul' {m n k : ℕ} :

m ≤ k * n → m / k ≤ n

Alias of Nat.div_le_of_le_mul.

source

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

source

theorem Nat.two_mul_odd_div_two {n : ℕ} (hn : n % 2 = 1) :

2 * (n / 2) = n - 1

`pow` #

source

theorem Nat.one_le_pow' (n m : ℕ) :

1 ≤ (m + 1) ^ n

source

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.

source

@[simp]

theorem Nat.rec_zero {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) :

rec h0 h 0 = h0

source

theorem Nat.rec_add_one {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) (n : ℕ) :

rec h0 h (n + 1) = h n (rec h0 h n)

source

@[simp]

theorem Nat.rec_one {C : ℕ → Sort u_1} (h0 : C 0) (h : (n : ℕ) → C n → C (n + 1)) :

rec h0 h 1 = h 0 h0

source

def Nat.leRec {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (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

source

theorem Nat.leRec_eq_leRec :

@leRec = @le.rec

source

@[simp]

theorem Nat.leRec_self {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) :

leRec refl le_succ_of_le ⋯ = refl

source

@[simp]

theorem Nat.leRec_succ {m n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (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)

source

theorem Nat.leRec_succ' {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (k + 1) ⋯) :

leRec refl le_succ_of_le ⋯ = le_succ_of_le ⋯ refl

source

theorem Nat.leRec_trans {n m k : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (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

source

theorem Nat.leRec_succ_left {n : ℕ} {motive : (m : ℕ) → n ≤ m → Sort u_1} (refl : motive n ⋯) (le_succ_of_le : ⦃k : ℕ⦄ → (h : n ≤ k) → motive k h → motive (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

source

def Nat.leRecOn {C : ℕ → Sort u_1} {n m : ℕ} :

n ≤ m → ({k : ℕ} → C k → C (k + 1)) → C n → C 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

Nat.leRecOn h of_succ self = Nat.leRec self (fun (x : ℕ) (x_1 : n ≤ x) => of_succ) h

Instances For

source

theorem Nat.leRecOn_self {C : ℕ → Sort u_1} {n : ℕ} {next : {k : ℕ} → C k → C (k + 1)} (x : C n) :

leRecOn ⋯ (fun {k : ℕ} => next) x = x

source

theorem Nat.leRecOn_succ {C : ℕ → Sort u_1} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n) :

leRecOn h2 next x = next (leRecOn h1 (fun {k : ℕ} => next) x)

source

theorem Nat.leRecOn_succ' {C : ℕ → Sort u_1} {n : ℕ} {h : n ≤ n + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n) :

leRecOn h (fun {k : ℕ} => next) x = next x

source

theorem Nat.leRecOn_trans {C : ℕ → Sort u_1} {n m k : ℕ} (hnm : n ≤ m) (hmk : m ≤ k) {next : {k : ℕ} → C k → C (k + 1)} (x : C n) :

leRecOn ⋯ next x = leRecOn hmk next (leRecOn hnm next x)

source

theorem Nat.leRecOn_succ_left {C : ℕ → Sort u_1} {n m : ℕ} {next : {k : ℕ} → C k → C (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

source

@[irreducible]

def Nat.strongRec' {p : ℕ → Sort u_1} (H : (n : ℕ) → ((m : ℕ) → m < n → p m) → p n) (n : ℕ) :

p n

Recursion principle based on <.

Equations

Nat.strongRec' H x✝ = H x✝ fun (m : ℕ) (x : m < x✝) => Nat.strongRec' H m

Instances For

source

def Nat.strongRecOn' {P : ℕ → Sort u_1} (n : ℕ) (h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n) :

P n

Recursion principle based on < applied to some natural number.

Equations

n.strongRecOn' h = Nat.strongRec' h n

Instances For

source

theorem Nat.strongRecOn'_beta {n : ℕ} {P : ℕ → Sort u_1} {h : (n : ℕ) → ((m : ℕ) → m < n → P m) → P n} :

n.strongRecOn' h = h n fun (m : ℕ) (x : m < n) => m.strongRecOn' h

source

theorem Nat.le_induction {m : ℕ} {P : (n : ℕ) → m ≤ n → Prop} (base : P m ⋯) (succ : ∀ (n : ℕ) (hmn : m ≤ n), P n hmn → P (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.

source

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

P a

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

Equations

Nat.twoStepInduction zero one more 0 = zero
Nat.twoStepInduction zero one more 1 = one
Nat.twoStepInduction zero one more n.succ.succ = more n (Nat.twoStepInduction zero one more n) (Nat.twoStepInduction zero one more (n + 1))

Instances For

source

theorem Nat.strong_induction_on {p : ℕ → Prop} (n : ℕ) (h : ∀ (n : ℕ), (∀ (m : ℕ), m < n → p m) → p n) :

p n

source

theorem Nat.case_strong_induction_on {p : ℕ → Prop} (a : ℕ) (hz : p 0) (hi : ∀ (n : ℕ), (∀ (m : ℕ), m ≤ n → p m) → p (n + 1)) :

p a

source

def Nat.decreasingInduction {n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive 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

source

@[simp]

theorem Nat.decreasingInduction_self {n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive k ⋯) (self : motive n ⋯) :

decreasingInduction of_succ self ⋯ = self

source

theorem Nat.decreasingInduction_succ {m n : ℕ} {motive : (m : ℕ) → m ≤ n + 1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive 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

source

@[simp]

theorem Nat.decreasingInduction_succ' {n : ℕ} {motive : (m : ℕ) → m ≤ n + 1 → Sort u_1} (of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯) (self : motive (n + 1) ⋯) :

decreasingInduction of_succ self ⋯ = of_succ n ⋯ self

source

theorem Nat.decreasingInduction_trans {m n k : ℕ} {motive : (m : ℕ) → m ≤ k → Sort u_1} (hmn : m ≤ n) (hnk : n ≤ k) (of_succ : (k_1 : ℕ) → (h : k_1 < k) → motive (k_1 + 1) h → motive 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

source

theorem Nat.decreasingInduction_succ_left {m n : ℕ} {motive : (m : ℕ) → m ≤ n → Sort u_1} (of_succ : (k : ℕ) → (h : k < n) → motive (k + 1) h → motive 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)

source

@[irreducible]

def Nat.strongSubRecursion {P : ℕ → ℕ → Sort u_1} (H : (m n : ℕ) → ((x y : ℕ) → x < m → y < n → P 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

Nat.strongSubRecursion H x✝¹ x✝ = H x✝¹ x✝ fun (x y : ℕ) (x_1 : x < x✝¹) (x_2 : y < x✝) => Nat.strongSubRecursion H x y

Instances For

source

@[irreducible]

def Nat.pincerRecursion {P : ℕ → ℕ → Sort u_1} (Ha0 : (m : ℕ) → P m 0) (H0b : (n : ℕ) → P 0 n) (H : (x y : ℕ) → P x y.succ → P x.succ y → P 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

Nat.pincerRecursion Ha0 H0b H x✝ 0 = Ha0 x✝
Nat.pincerRecursion Ha0 H0b H 0 x✝ = H0b x✝
Nat.pincerRecursion Ha0 H0b H n.succ n_1.succ = H n n_1 (Nat.pincerRecursion Ha0 H0b H n n_1.succ) (Nat.pincerRecursion Ha0 H0b H n.succ n_1)

Instances For

source

def Nat.decreasingInduction' {m n : ℕ} {P : ℕ → Sort u_1} (h : (k : ℕ) → k < n → m ≤ k → P (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

source

@[irreducible]

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.

`mod`, `dvd` #

source

theorem Nat.not_pos_pow_dvd {a n : ℕ} (ha : 1 < a) (hn : 1 < n) :

¬a ^ n ∣ a

source

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

source

@[simp]

theorem Nat.not_two_dvd_bit1 (n : ℕ) :

¬2 ∣ 2 * n + 1

source

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

source

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

source

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

source

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.

source

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 #

source

instance Nat.decidableLoHi (lo hi : ℕ) (P : ℕ → Prop) [DecidablePred P] :

Decidable (∀ (x : ℕ), lo ≤ x → x < hi → P x)

Equations

lo.decidableLoHi hi P = decidable_of_iff (∀ (x : ℕ), x < hi - lo → P (lo + x)) ⋯

source

instance Nat.decidableLoHiLe (lo hi : ℕ) (P : ℕ → Prop) [DecidablePred P] :

Decidable (∀ (x : ℕ), lo ≤ x → x ≤ hi → P x)

Equations

lo.decidableLoHiLe hi P = decidable_of_iff (∀ (x : ℕ), lo ≤ x → x < hi + 1 → P x) ⋯

`Nat.AtLeastTwo` #

source

class Nat.AtLeastTwo (n : ℕ) :

Prop

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.