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

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.succ → m ≤ 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 + 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.

@[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 ≠ 0 → n ≠ 1 → n ≠ 2 → 2 < 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 * n → m / 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 n → C (n + 1)) : rec h0 h 0 = h0

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)

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

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.

theorem Nat.leRec_eq_leRec : @leRec = @le.rec

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

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

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

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

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

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

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

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)

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

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)

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

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

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

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

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.

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

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

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

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.

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

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

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

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

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)

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

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

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.

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

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 ≤ x → x < hi → P x)

Equations

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

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

class Nat.AtLeastTwo (n : ℕ) : Prop

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

• prop : 2 ≤ n

instance Nat.instAtLeastTwo {n : ℕ} : (n + 2).AtLeastTwo

instance Nat.instAtLeastTwoHAddOfNat {n : ℕ} [NeZero n] : (n + 1).AtLeastTwo

theorem Nat.AtLeastTwo.one_lt {n : ℕ} [n.AtLeastTwo] : 1 < n

theorem Nat.AtLeastTwo.ne_one {n : ℕ} [n.AtLeastTwo] : n ≠ 1