Documentation

Init.Data.Nat.Basic

def Nat.recCompiled {motive : Nat → Sort u} (zero : motive zero) (succ : (n : Nat) → motive n → motive n.succ) (t : Nat) :

motive t

Compiled version of Nat.rec so that we can define Nat.recAux to be defeq to Nat.rec. This is working around the fact that the compiler does not currently support recursors.

Equations

Instances For

@[csimp]

theorem Nat.rec_eq_recCompiled :

@rec = @recCompiled

@[reducible, inline]

abbrev Nat.recAux {motive : Nat → Sort u} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (t : Nat) :

motive t

A recursor for Nat that uses the notations 0 for Nat.zero and n + 1 for Nat.succ.

It is otherwise identical to the default recursor Nat.rec. It is used by the induction tactic by default for Nat.

Equations

Instances For

@[reducible, inline]

abbrev Nat.casesAuxOn {motive : Nat → Sort u} (t : Nat) (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) :

motive t

A case analysis principle for Nat that uses the notations 0 for Nat.zero and n + 1 for Nat.succ.

It is otherwise identical to the default recursor Nat.casesOn. It is used as the default Nat case analysis principle for Nat by the cases tactic.

Equations

Instances For

@[specialize #[]]

def Nat.repeat {α : Type u} (f : α → α) (n : Nat) (a : α) :

α

Applies a function to a starting value the specified number of times.

In other words, f is iterated n times on a.

Examples:

Nat.repeat f 3 a = f <| f <| f <| a
Nat.repeat (· ++ "!") 4 "Hello" = "Hello!!!!"

Equations

Instances For

@[inline]

def Nat.repeatTR {α : Type u} (f : α → α) (n : Nat) (a : α) :

α

Applies a function to a starting value the specified number of times.

In other words, f is iterated n times on a.

This is a tail-recursive version of Nat.repeat that's used at runtime.

Examples:

Nat.repeatTR f 3 a = f <| f <| f <| a
Nat.repeatTR (· ++ "!") 4 "Hello" = "Hello!!!!"

Equations

Instances For

def Nat.blt (a b : Nat) :

The Boolean less-than comparison on natural numbers.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the arbitrary-precision arithmetic library. The definition provided here is the logical model.

Examples:

Nat.blt 2 5 = true
Nat.blt 5 2 = false
Nat.blt 5 5 = false

Equations

Instances For

theorem Nat.and_forall_add_one {p : Nat → Prop} :

(p 0 ∧ ∀ (n : Nat), p (n + 1)) ↔ ∀ (n : Nat), p n

theorem Nat.or_exists_add_one {p : Nat → Prop} :

(p 0 ∨ ∃ (n : Nat ), p (n + 1)) ↔ Exists p

Helper "packing" theorems #

@[simp]

theorem Nat.zero_eq :

@[simp]

theorem Nat.add_eq {x y : Nat} :

x.add y = x + y

@[simp]

theorem Nat.mul_eq {x y : Nat} :

x.mul y = x * y

@[simp]

theorem Nat.sub_eq {x y : Nat} :

x.sub y = x - y

@[simp]

theorem Nat.lt_eq {x y : Nat} :

x.lt y = (x < y)

@[simp]

theorem Nat.le_eq {x y : Nat} :

x.le y = (x ≤ y)

Helper Bool relation theorems #

@[simp]

theorem Nat.beq_refl (a : Nat) :

@[simp]

theorem Nat.beq_eq {x y : Nat} :

(x.beq y = true) = (x = y)

@[simp]

theorem Nat.ble_eq {x y : Nat} :

(x.ble y = true) = (x ≤ y)

@[simp]

theorem Nat.blt_eq {x y : Nat} :

(x.blt y = true) = (x < y)

instance Nat.instLawfulBEq :

theorem Nat.beq_eq_true_eq (a b : Nat) :

((a == b) = true) = (a = b)

theorem Nat.not_beq_eq_true_eq (a b : Nat) :

((!a == b) = true) = ¬a = b

Nat.add theorems #

@[simp]

theorem Nat.zero_add (n : Nat) :

0 + n = n

instance Nat.instLawfulIdentityHAddOfNat :

Std.LawfulIdentity (fun (x1 x2 : Nat) => x1 + x2) 0

theorem Nat.succ_add (n m : Nat) :

n.succ + m = (n + m).succ

theorem Nat.add_succ (n m : Nat) :

n + m.succ = (n + m).succ

theorem Nat.add_one (n : Nat) :

n + 1 = n.succ

@[simp]

theorem Nat.succ_eq_add_one (n : Nat) :

n.succ = n + 1

theorem Nat.add_one_ne_zero (n : Nat) :

n + 1 ≠ 0

theorem Nat.zero_ne_add_one (n : Nat) :

0 ≠ n + 1

theorem Nat.add_comm (n m : Nat) :

n + m = m + n

instance Nat.instCommutativeHAdd :

Std.Commutative fun (x1 x2 : Nat) => x1 + x2

theorem Nat.add_assoc (n m k : Nat) :

n + m + k = n + (m + k)

instance Nat.instAssociativeHAdd :

Std.Associative fun (x1 x2 : Nat) => x1 + x2

theorem Nat.add_left_comm (n m k : Nat) :

n + (m + k) = m + (n + k)

theorem Nat.add_right_comm (n m k : Nat) :

n + m + k = n + k + m

theorem Nat.add_left_cancel {n m k : Nat} :

n + m = n + k → m = k

theorem Nat.add_right_cancel {n m k : Nat} (h : n + m = k + m) :

n = k

theorem Nat.eq_zero_of_add_eq_zero {n m : Nat} :

n + m = 0 → n = 0 ∧ m = 0

theorem Nat.eq_zero_of_add_eq_zero_left {n m : Nat} (h : n + m = 0) :

m = 0

Nat.mul theorems #

@[simp]

theorem Nat.mul_zero (n : Nat) :

n * 0 = 0

theorem Nat.mul_succ (n m : Nat) :

n * m.succ = n * m + n

theorem Nat.mul_add_one (n m : Nat) :

n * (m + 1) = n * m + n

@[simp]

theorem Nat.zero_mul (n : Nat) :

0 * n = 0

theorem Nat.succ_mul (n m : Nat) :

n.succ * m = n * m + m

theorem Nat.add_one_mul (n m : Nat) :

(n + 1) * m = n * m + m

theorem Nat.mul_comm (n m : Nat) :

n * m = m * n

instance Nat.instCommutativeHMul :

Std.Commutative fun (x1 x2 : Nat) => x1 * x2

@[simp]

theorem Nat.mul_one (n : Nat) :

n * 1 = n

@[simp]

theorem Nat.one_mul (n : Nat) :

1 * n = n

instance Nat.instLawfulIdentityHMulOfNat :

Std.LawfulIdentity (fun (x1 x2 : Nat) => x1 * x2) 1

theorem Nat.left_distrib (n m k : Nat) :

n * (m + k) = n * m + n * k

theorem Nat.right_distrib (n m k : Nat) :

(n + m) * k = n * k + m * k

theorem Nat.mul_add (n m k : Nat) :

n * (m + k) = n * m + n * k

theorem Nat.add_mul (n m k : Nat) :

(n + m) * k = n * k + m * k

theorem Nat.mul_assoc (n m k : Nat) :

n * m * k = n * (m * k)

instance Nat.instAssociativeHMul :

Std.Associative fun (x1 x2 : Nat) => x1 * x2

theorem Nat.mul_left_comm (n m k : Nat) :

n * (m * k) = m * (n * k)

theorem Nat.mul_two (n : Nat) :

n * 2 = n + n

theorem Nat.two_mul (n : Nat) :

2 * n = n + n

Inequalities #

@[deprecated Nat.le_succ_of_le (since := "2025-10-26")]

theorem Nat.le_step {n m : Nat} (h : n ≤ m) :

theorem Nat.succ_lt_succ {n m : Nat} :

n < m → n.succ < m.succ

theorem Nat.le_of_lt_add_one {n m : Nat} :

n < m + 1 → n ≤ m

theorem Nat.lt_add_one_of_le {n m : Nat} :

n ≤ m → n < m + 1

@[simp]

theorem Nat.sub_zero (n : Nat) :

n - 0 = n

theorem Nat.not_add_one_le_zero (n : Nat) :

¬n + 1 ≤ 0

theorem Nat.not_add_one_le_self (n : Nat) :

¬n + 1 ≤ n

theorem Nat.add_one_pos (n : Nat) :

0 < n + 1

theorem Nat.pred_lt {n : Nat} :

n ≠ 0 → n.pred < n

theorem Nat.sub_one_lt {n : Nat} :

n ≠ 0 → n - 1 < n

theorem Nat.sub_lt_of_lt {a b c : Nat} (h : a < c) :

a - b < c

theorem Nat.sub_succ (n m : Nat) :

n - m.succ = (n - m).pred

theorem Nat.succ_sub_succ (n m : Nat) :

n.succ - m.succ = n - m

@[simp]

theorem Nat.sub_self (n : Nat) :

n - n = 0

theorem Nat.sub_add_eq (a b c : Nat) :

a - (b + c) = a - b - c

theorem Nat.lt_of_lt_of_eq {n m k : Nat} :

n < m → m = k → n < k

instance Nat.instTransLt :

Trans (fun (x1 x2 : Nat) => x1 < x2) (fun (x1 x2 : Nat) => x1 < x2) fun (x1 x2 : Nat) => x1 < x2

Equations

instance Nat.instTransLe :

Trans (fun (x1 x2 : Nat) => x1 ≤ x2) (fun (x1 x2 : Nat) => x1 ≤ x2) fun (x1 x2 : Nat) => x1 ≤ x2

Equations

instance Nat.instTransLtLe :

Trans (fun (x1 x2 : Nat) => x1 < x2) (fun (x1 x2 : Nat) => x1 ≤ x2) fun (x1 x2 : Nat) => x1 < x2

Equations

instance Nat.instTransLeLt :

Trans (fun (x1 x2 : Nat) => x1 ≤ x2) (fun (x1 x2 : Nat) => x1 < x2) fun (x1 x2 : Nat) => x1 < x2

Equations

theorem Nat.le_of_eq {n m : Nat} (p : n = m) :

n ≤ m

theorem Nat.le_of_succ_le {n m : Nat} (h : n.succ ≤ m) :

n ≤ m

theorem Nat.lt_of_succ_lt {n m : Nat} :

n.succ < m → n < m

theorem Nat.le_of_lt {n m : Nat} :

n < m → n ≤ m

theorem Nat.lt_of_succ_lt_succ {n m : Nat} :

n.succ < m.succ → n < m

theorem Nat.lt_of_succ_le {n m : Nat} (h : n.succ ≤ m) :

n < m

theorem Nat.succ_le_of_lt {n m : Nat} (h : n < m) :

theorem Nat.succ_le_iff {m n : Nat} :

m.succ ≤ n ↔ m < n

theorem Nat.eq_zero_or_pos (n : Nat) :

n = 0 ∨ n > 0

theorem Nat.pos_of_ne_zero {n : Nat} :

n ≠ 0 → 0 < n

theorem Nat.pos_of_neZero (n : Nat) [NeZero n] :

0 < n

@[deprecated Nat.lt_add_one (since := "2025-10-26")]

theorem Nat.lt.base (n : Nat) :

n < n.succ

theorem Nat.le_total (m n : Nat) :

m ≤ n ∨ n ≤ m

theorem Nat.eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) :

n = 0

theorem Nat.zero_lt_of_lt {a b : Nat} :

a < b → 0 < b

theorem Nat.zero_lt_of_ne_zero {a : Nat} (h : a ≠ 0) :

0 < a

theorem Nat.ne_of_lt {a b : Nat} (h : a < b) :

a ≠ b

theorem Nat.le_or_eq_of_le_succ {m n : Nat} (h : m ≤ n.succ) :

m ≤ n ∨ m = n.succ

theorem Nat.le_or_eq_of_le_add_one {m n : Nat} (h : m ≤ n + 1) :

m ≤ n ∨ m = n + 1

@[simp]

theorem Nat.le_add_right (n k : Nat) :

n ≤ n + k

@[simp]

theorem Nat.le_add_left (n m : Nat) :

n ≤ m + n

theorem Nat.le_of_add_right_le {n m k : Nat} (h : n + k ≤ m) :

n ≤ m

theorem Nat.le_add_right_of_le {n m k : Nat} (h : n ≤ m) :

n ≤ m + k

theorem Nat.le_of_add_left_le {n m k : Nat} (h : k + n ≤ m) :

n ≤ m

theorem Nat.le_add_left_of_le {n m k : Nat} (h : n ≤ m) :

n ≤ k + m

theorem Nat.lt_of_add_one_le {n m : Nat} (h : n + 1 ≤ m) :

n < m

theorem Nat.add_one_le_of_lt {n m : Nat} (h : n < m) :

n + 1 ≤ m

theorem Nat.lt_add_left {a b : Nat} (c : Nat) (h : a < b) :

a < c + b

theorem Nat.lt_add_right {a b : Nat} (c : Nat) (h : a < b) :

a < b + c

theorem Nat.lt_of_add_right_lt {n m k : Nat} (h : n + k < m) :

n < m

theorem Nat.lt_of_add_left_lt {n m k : Nat} (h : k + n < m) :

n < m

theorem Nat.le.dest {n m : Nat} :

n ≤ m → ∃ (k : Nat ), n + k = m

theorem Nat.le.intro {n m k : Nat} (h : n + k = m) :

n ≤ m

theorem Nat.not_le_of_gt {n m : Nat} (h : n > m) :

theorem Nat.not_le_of_lt {a b : Nat} :

a < b → ¬b ≤ a

theorem Nat.not_lt_of_ge {a b : Nat} :

b ≥ a → ¬b < a

theorem Nat.not_lt_of_le {a b : Nat} :

a ≤ b → ¬b < a

theorem Nat.lt_le_asymm {a b : Nat} :

a < b → ¬b ≤ a

theorem Nat.le_lt_asymm {a b : Nat} :

a ≤ b → ¬b < a

theorem Nat.gt_of_not_le {n m : Nat} (h : ¬n ≤ m) :

n > m

theorem Nat.lt_of_not_ge {a b : Nat} :

¬b ≥ a → b < a

theorem Nat.ge_of_not_lt {n m : Nat} (h : ¬n < m) :

n ≥ m

theorem Nat.le_of_not_gt {a b : Nat} :

¬b > a → b ≤ a

theorem Nat.le_of_not_lt {a b : Nat} :

¬a < b → b ≤ a

theorem Nat.ne_of_gt {a b : Nat} (h : b < a) :

a ≠ b

theorem Nat.ne_of_lt' {a b : Nat} :

a < b → b ≠ a

@[simp]

theorem Nat.not_le {a b : Nat} :

¬a ≤ b ↔ b < a

@[simp]

theorem Nat.not_lt {a b : Nat} :

¬a < b ↔ b ≤ a

theorem Nat.le_of_not_le {a b : Nat} (h : ¬b ≤ a) :

a ≤ b

theorem Nat.le_of_not_ge {a b : Nat} :

¬a ≥ b → a ≤ b

theorem Nat.lt_trichotomy (a b : Nat) :

a < b ∨ a = b ∨ b < a

theorem Nat.lt_or_gt_of_ne {a b : Nat} (ne : a ≠ b) :

a < b ∨ a > b

theorem Nat.lt_or_lt_of_ne {a b : Nat} :

a ≠ b → a < b ∨ b < a

theorem Nat.le_antisymm_iff {a b : Nat} :

a = b ↔ a ≤ b ∧ b ≤ a

theorem Nat.eq_iff_le_and_ge {a b : Nat} :

a = b ↔ a ≤ b ∧ b ≤ a

instance Nat.instAntisymmLe :

Std.Antisymm fun (x1 x2 : Nat) => x1 ≤ x2

instance Nat.instTrichotomousLt :

Std.Trichotomous fun (x1 x2 : Nat) => x1 < x2

@[deprecated Nat.instTrichotomousLt (since := "2025-10-27")]

def Nat.Nat.instAntisymmNotLt :

Std.Antisymm fun (x1 x2 : Nat) => ¬x1 < x2

Equations

Instances For

theorem Nat.add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) :

k + n ≤ k + m

theorem Nat.add_le_add_right {n m : Nat} (h : n ≤ m) (k : Nat) :

n + k ≤ m + k

theorem Nat.add_lt_add_left {n m : Nat} (h : n < m) (k : Nat) :

k + n < k + m

theorem Nat.add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) :

n + k < m + k

theorem Nat.lt_add_of_pos_left {k n : Nat} (h : 0 < k) :

n < k + n

theorem Nat.lt_add_of_pos_right {k n : Nat} (h : 0 < k) :

n < n + k

theorem Nat.zero_lt_one :

0 < 1

theorem Nat.pos_iff_ne_zero {n : Nat} :

0 < n ↔ n ≠ 0

theorem Nat.add_le_add {a b c d : Nat} (h₁ : a ≤ b) (h₂ : c ≤ d) :

a + c ≤ b + d

theorem Nat.add_lt_add {a b c d : Nat} (h₁ : a < b) (h₂ : c < d) :

a + c < b + d

theorem Nat.le_of_add_le_add_left {a b c : Nat} (h : a + b ≤ a + c) :

b ≤ c

theorem Nat.le_of_add_le_add_right {a b c : Nat} :

a + b ≤ c + b → a ≤ c

@[simp]

theorem Nat.add_le_add_iff_right {m k n : Nat} :

m + n ≤ k + n ↔ m ≤ k

@[simp]

theorem Nat.add_le_add_iff_left {m k n : Nat} :

n + m ≤ n + k ↔ m ≤ k

le/lt #

theorem Nat.lt_asymm {a b : Nat} (h : a < b) :

¬b < a

@[reducible, inline]

abbrev Nat.not_lt_of_gt {a b : Nat} (h : a < b) :

¬b < a

Alias for Nat.lt_asymm.

Equations

Instances For

@[reducible, inline]

abbrev Nat.not_lt_of_lt {a b : Nat} (h : a < b) :

¬b < a

Alias for Nat.lt_asymm.

Equations

Instances For

theorem Nat.lt_iff_le_not_le {m n : Nat} :

m < n ↔ m ≤ n ∧ ¬n ≤ m

@[reducible, inline]

abbrev Nat.lt_iff_le_and_not_ge {m n : Nat} :

m < n ↔ m ≤ n ∧ ¬n ≤ m

Alias for Nat.lt_iff_le_not_le.

Equations

Instances For

theorem Nat.lt_iff_le_and_ne {m n : Nat} :

m < n ↔ m ≤ n ∧ m ≠ n

theorem Nat.ne_iff_lt_or_gt {a b : Nat} :

a ≠ b ↔ a < b ∨ b < a

@[reducible, inline]

abbrev Nat.lt_or_gt {a b : Nat} :

a ≠ b ↔ a < b ∨ b < a

Alias for Nat.ne_iff_lt_or_gt.

Equations

Instances For

@[reducible, inline]

abbrev Nat.le_or_ge (m n : Nat) :

m ≤ n ∨ n ≤ m

Alias for Nat.le_total.

Equations

Instances For

@[reducible, inline]

abbrev Nat.le_or_le (m n : Nat) :

m ≤ n ∨ n ≤ m

Alias for Nat.le_total.

Equations

Instances For

theorem Nat.eq_or_lt_of_not_lt {a b : Nat} (hnlt : ¬a < b) :

a = b ∨ b < a

theorem Nat.lt_or_eq_of_le {n m : Nat} (h : n ≤ m) :

n < m ∨ n = m

theorem Nat.le_iff_lt_or_eq {n m : Nat} :

n ≤ m ↔ n < m ∨ n = m

theorem Nat.lt_succ_iff {m n : Nat} :

m < n.succ ↔ m ≤ n

theorem Nat.lt_add_one_iff {m n : Nat} :

m < n + 1 ↔ m ≤ n

theorem Nat.lt_succ_iff_lt_or_eq {m n : Nat} :

m < n.succ ↔ m < n ∨ m = n

theorem Nat.lt_add_one_iff_lt_or_eq {m n : Nat} :

m < n + 1 ↔ m < n ∨ m = n

theorem Nat.eq_of_lt_succ_of_not_lt {m n : Nat} (hmn : m < n + 1) (h : ¬m < n) :

m = n

theorem Nat.eq_of_le_of_lt_succ {n m : Nat} (h₁ : n ≤ m) (h₂ : m < n + 1) :

m = n

zero/one/two #

theorem Nat.le_zero {i : Nat} :

i ≤ 0 ↔ i = 0

@[reducible, inline]

abbrev Nat.one_pos :

0 < 1

Alias for Nat.zero_lt_one.

Equations

Instances For

theorem Nat.two_pos :

0 < 2

theorem Nat.ne_zero_iff_zero_lt {n : Nat} :

n ≠ 0 ↔ 0 < n

theorem Nat.zero_lt_two :

0 < 2

theorem Nat.one_lt_two :

1 < 2

theorem Nat.eq_zero_of_not_pos {n : Nat} (h : ¬0 < n) :

n = 0

succ/pred #

@[simp]

theorem Nat.succ_ne_self (n : Nat) :

theorem Nat.add_one_ne_self (n : Nat) :

n + 1 ≠ n

theorem Nat.add_one_le_iff {n m : Nat} :

n + 1 ≤ m ↔ n < m

@[deprecated Nat.lt_succ_iff (since := "2025-10-26")]

theorem Nat.lt_succ {m n : Nat} :

m < n.succ ↔ m ≤ n

theorem Nat.lt_succ_of_lt {a b : Nat} (h : a < b) :

a < b.succ

@[deprecated Nat.lt_succ_of_lt (since := "2025-10-26")]

theorem Nat.lt.step {n m : Nat} :

n < m → n < m.succ

theorem Nat.lt_add_one_of_lt {a b : Nat} (h : a < b) :

a < b + 1

@[simp]

theorem Nat.lt_one_iff {n : Nat} :

n < 1 ↔ n = 0

theorem Nat.succ_pred_eq_of_ne_zero {n : Nat} :

n ≠ 0 → n.pred.succ = n

theorem Nat.eq_zero_or_eq_succ_pred (n : Nat) :

n = 0 ∨ n = n.pred.succ

theorem Nat.succ_inj {a b : Nat} :

a.succ = b.succ ↔ a = b

theorem Nat.succ_le_succ_iff {a b : Nat} :

a.succ ≤ b.succ ↔ a ≤ b

theorem Nat.succ_lt_succ_iff {a b : Nat} :

a.succ < b.succ ↔ a < b

theorem Nat.succ_ne_succ_iff {a b : Nat} :

a.succ ≠ b.succ ↔ a ≠ b

theorem Nat.succ_succ_ne_one (a : Nat) :

a.succ.succ ≠ 1

theorem Nat.add_one_inj {a b : Nat} :

a + 1 = b + 1 ↔ a = b

theorem Nat.ne_add_one (n : Nat) :

n ≠ n + 1

@[deprecated Nat.add_one_ne_self (since := "2025-10-26")]

theorem Nat.add_one_ne (n : Nat) :

n + 1 ≠ n

theorem Nat.add_one_le_add_one_iff {a b : Nat} :

a + 1 ≤ b + 1 ↔ a ≤ b

theorem Nat.add_one_lt_add_one_iff {a b : Nat} :

a + 1 < b + 1 ↔ a < b

theorem Nat.add_one_ne_add_one_iff {a b : Nat} :

a + 1 ≠ b + 1 ↔ a ≠ b

theorem Nat.add_one_add_one_ne_one {a : Nat} :

a + 1 + 1 ≠ 1

theorem Nat.pred_inj {a b : Nat} :

0 < a → 0 < b → a.pred = b.pred → a = b

theorem Nat.pred_ne_self {a : Nat} :

a ≠ 0 → a.pred ≠ a

theorem Nat.sub_one_ne_self {a : Nat} :

a ≠ 0 → a - 1 ≠ a

theorem Nat.pred_lt_self {a : Nat} :

0 < a → a.pred < a

theorem Nat.pred_lt_pred {n m : Nat} :

n ≠ 0 → n < m → n.pred < m.pred

theorem Nat.pred_le_iff {n : Nat} {m : Nat} :

n.pred ≤ m ↔ n ≤ m.succ

@[deprecated Nat.pred_le_iff (since := "2025-10-26")]

theorem Nat.pred_le_iff_le_succ {n : Nat} {m : Nat} :

n.pred ≤ m ↔ n ≤ m.succ

theorem Nat.le_succ_of_pred_le {n : Nat} {m : Nat} :

n.pred ≤ m → n ≤ m.succ

theorem Nat.pred_le_of_le_succ {n m : Nat} :

n ≤ m.succ → n.pred ≤ m

theorem Nat.lt_pred_iff {n : Nat} {m : Nat} :

n < m.pred ↔ n.succ < m

@[deprecated Nat.lt_pred_iff (since := "2025-10-26")]

theorem Nat.lt_pred_iff_succ_lt {n : Nat} {m : Nat} :

n < m.pred ↔ n.succ < m

theorem Nat.succ_lt_of_lt_pred {n : Nat} {m : Nat} :

n < m.pred → n.succ < m

theorem Nat.lt_pred_of_succ_lt {n m : Nat} :

n.succ < m → n < m.pred

theorem Nat.le_pred_iff_lt {n : Nat} {m : Nat} :

0 < m → (n ≤ m.pred ↔ n < m)

theorem Nat.le_pred_of_lt {n m : Nat} (h : n < m) :

theorem Nat.le_sub_one_of_lt {a b : Nat} :

a < b → a ≤ b - 1

theorem Nat.lt_of_le_pred {m : Nat} {n : Nat} (h : 0 < m) :

n ≤ m.pred → n < m

theorem Nat.lt_of_le_sub_one {m n : Nat} (h : 0 < m) :

n ≤ m - 1 → n < m

theorem Nat.le_sub_one_iff_lt {m n : Nat} (h : 0 < m) :

n ≤ m - 1 ↔ n < m

theorem Nat.exists_eq_succ_of_ne_zero {n : Nat} :

n ≠ 0 → ∃ (k : Nat ), n = k.succ

theorem Nat.exists_eq_add_one_of_ne_zero {n : Nat} :

n ≠ 0 → ∃ (k : Nat ), n = k + 1

Basic theorems for comparing numerals #

@[deprecated Nat.zero_eq (since := "2025-10-26")]

theorem Nat.ctor_eq_zero :

theorem Nat.one_ne_zero :

1 ≠ 0

@[simp]

theorem Nat.zero_ne_one :

0 ≠ 1

theorem Nat.succ_ne_zero (n : Nat) :

instance Nat.instNeZeroSucc {n : Nat} :

NeZero (n + 1)

@[simp]

theorem Nat.default_eq_zero :

mul + order #

theorem Nat.mul_le_mul_left {n m : Nat} (k : Nat) (h : n ≤ m) :

k * n ≤ k * m

theorem Nat.mul_le_mul_right {n m : Nat} (k : Nat) (h : n ≤ m) :

n * k ≤ m * k

theorem Nat.mul_le_mul {n₁ m₁ n₂ m₂ : Nat} (h₁ : n₁ ≤ n₂) (h₂ : m₁ ≤ m₂) :

n₁ * m₁ ≤ n₂ * m₂

theorem Nat.mul_lt_mul_of_pos_left {n m k : Nat} (h : n < m) (hk : k > 0) :

k * n < k * m

theorem Nat.mul_lt_mul_of_pos_right {n m k : Nat} (h : n < m) (hk : k > 0) :

n * k < m * k

theorem Nat.le_of_mul_le_mul_left {a b c : Nat} (h : c * a ≤ c * b) (hc : 0 < c) :

a ≤ b

theorem Nat.le_of_mul_le_mul_right {a b c : Nat} (h : a * c ≤ b * c) (hc : 0 < c) :

a ≤ b

theorem Nat.mul_le_mul_left_iff {n m k : Nat} (w : 0 < k) :

k * n ≤ k * m ↔ n ≤ m

theorem Nat.mul_le_mul_right_iff {n m k : Nat} (w : 0 < k) :

n * k ≤ m * k ↔ n ≤ m

theorem Nat.eq_of_mul_eq_mul_left {m k n : Nat} (hn : 0 < n) (h : n * m = n * k) :

m = k

theorem Nat.eq_of_mul_eq_mul_right {n m k : Nat} (hm : 0 < m) (h : n * m = k * m) :

n = k

power #

theorem Nat.pow_succ (n m : Nat) :

n ^ m.succ = n ^ m * n

theorem Nat.pow_add_one (n m : Nat) :

n ^ (m + 1) = n ^ m * n

@[simp]

theorem Nat.pow_zero (n : Nat) :

n ^ 0 = 1

@[simp]

theorem Nat.pow_one (a : Nat) :

a ^ 1 = a

theorem Nat.pow_le_pow_left {n m : Nat} (h : n ≤ m) (i : Nat) :

n ^ i ≤ m ^ i

theorem Nat.pow_le_pow_right {n : Nat} (hx : n > 0) {i j : Nat} :

i ≤ j → n ^ i ≤ n ^ j

@[simp]

theorem Nat.zero_pow_of_pos (n : Nat) (h : 0 < n) :

0 ^ n = 0

theorem Nat.two_pow_pos (w : Nat) :

0 < 2 ^ w

instance Nat.instNeZeroHPow {n m : Nat} [NeZero n] :

NeZero (n ^ m)

instance Nat.instNeZeroHPowOfNat {n : Nat} :

NeZero (n ^ 0)

theorem Nat.mul_pow (a b n : Nat) :

(a * b) ^ n = a ^ n * b ^ n

theorem Nat.pow_lt_pow_left {a b n : Nat} (hab : a < b) (h : n ≠ 0) :

a ^ n < b ^ n

theorem Nat.pow_left_inj {a b n : Nat} (hn : n ≠ 0) :

a ^ n = b ^ n ↔ a = b

min/max #

@[reducible, inline]

abbrev Nat.min (n m : Nat) :

Returns the lesser of two natural numbers. Usually accessed via Min.min.

Returns n if n ≤ m, or m if m ≤ n.

Examples:

min 0 5 = 0
min 4 5 = 4
min 4 3 = 3
min 8 8 = 8

Equations

Instances For

theorem Nat.min_def {n m : Nat} :

min n m = if n ≤ m then n else m

instance Nat.instMax :

Equations

@[reducible, inline]

abbrev Nat.max (n m : Nat) :

Returns the greater of two natural numbers. Usually accessed via Max.max.

Returns m if n ≤ m, or n if m ≤ n.

Examples:

max 0 5 = 5
max 4 5 = 5
max 4 3 = 4
max 8 8 = 8

Equations

Instances For

theorem Nat.max_def {n m : Nat} :

max n m = if n ≤ m then m else n

Auxiliary theorems for well-founded recursion #

theorem Nat.ne_zero_of_lt {b a : Nat} (h : b < a) :

a ≠ 0

theorem Nat.pred_lt_of_lt {n m : Nat} (h : m < n) :

n.pred < n

theorem Nat.sub_one_lt_of_lt {n m : Nat} (h : m < n) :

n - 1 < n

pred theorems #

theorem Nat.pred_zero :

pred 0 = 0

theorem Nat.pred_succ (n : Nat) :

n.succ.pred = n

@[simp]

theorem Nat.zero_sub_one :

0 - 1 = 0

@[simp]

theorem Nat.add_one_sub_one (n : Nat) :

n + 1 - 1 = n

theorem Nat.sub_one_eq_self {n : Nat} :

n - 1 = n ↔ n = 0

theorem Nat.eq_self_sub_one {n : Nat} :

n = n - 1 ↔ n = 0

theorem Nat.succ_pred {a : Nat} (h : a ≠ 0) :

a.pred.succ = a

theorem Nat.sub_one_add_one {a : Nat} (h : a ≠ 0) :

a - 1 + 1 = a

theorem Nat.succ_pred_eq_of_pos {n : Nat} :

0 < n → n.pred.succ = n

theorem Nat.sub_one_add_one_eq_of_pos {n : Nat} :

0 < n → n - 1 + 1 = n

theorem Nat.eq_zero_or_eq_sub_one_add_one {n : Nat} :

n = 0 ∨ n = n - 1 + 1

@[simp]

theorem Nat.pred_eq_sub_one {n : Nat} :

n.pred = n - 1

sub theorems #

theorem Nat.add_sub_self_left (a b : Nat) :

a + b - a = b

theorem Nat.add_sub_self_right (a b : Nat) :

a + b - b = a

theorem Nat.sub_le_succ_sub (a i : Nat) :

a - i ≤ a.succ - i

theorem Nat.zero_lt_sub_of_lt {i a : Nat} (h : i < a) :

0 < a - i

theorem Nat.sub_succ_lt_self (a i : Nat) (h : i < a) :

a - (i + 1) < a - i

theorem Nat.sub_ne_zero_of_lt {a b : Nat} :

a < b → b - a ≠ 0

theorem Nat.add_sub_of_le {a b : Nat} (h : a ≤ b) :

a + (b - a) = b

theorem Nat.sub_one_cancel {a b : Nat} :

0 < a → 0 < b → a - 1 = b - 1 → a = b

@[simp]

theorem Nat.sub_add_cancel {n m : Nat} (h : m ≤ n) :

n - m + m = n

theorem Nat.add_sub_add_right (n k m : Nat) :

n + k - (m + k) = n - m

theorem Nat.add_sub_add_left (k n m : Nat) :

k + n - (k + m) = n - m

@[simp]

theorem Nat.add_sub_cancel (n m : Nat) :

n + m - m = n

@[simp]

theorem Nat.add_sub_cancel_left (n m : Nat) :

n + m - n = m

theorem Nat.add_sub_assoc {m k : Nat} (h : k ≤ m) (n : Nat) :

n + m - k = n + (m - k)

theorem Nat.eq_add_of_sub_eq {a b c : Nat} (hle : b ≤ a) (h : a - b = c) :

a = c + b

theorem Nat.sub_eq_of_eq_add {a b c : Nat} (h : a = c + b) :

a - b = c

theorem Nat.le_add_of_sub_le {a b c : Nat} (h : a - b ≤ c) :

a ≤ c + b

theorem Nat.sub_lt_sub_left {k m n : Nat} :

k < m → k < n → m - n < m - k

@[simp]

theorem Nat.zero_sub (n : Nat) :

0 - n = 0

theorem Nat.sub_lt_sub_right {a b c : Nat} :

c ≤ a → a < b → a - c < b - c

theorem Nat.sub_self_add (n m : Nat) :

n - (n + m) = 0

@[simp]

theorem Nat.sub_eq_zero_of_le {n m : Nat} (h : n ≤ m) :

n - m = 0

theorem Nat.sub_le_of_le_add {a b c : Nat} (h : a ≤ c + b) :

a - b ≤ c

theorem Nat.add_le_of_le_sub {a b c : Nat} (hle : b ≤ c) (h : a ≤ c - b) :

a + b ≤ c

theorem Nat.le_sub_of_add_le {a b c : Nat} (h : a + b ≤ c) :

a ≤ c - b

theorem Nat.add_lt_of_lt_sub {a b c : Nat} (h : a < c - b) :

a + b < c

theorem Nat.lt_sub_of_add_lt {a b c : Nat} (h : a + b < c) :

a < c - b

theorem Nat.sub.elim {motive : Nat → Prop} (x y : Nat) (h₁ : y ≤ x → ∀ (k : Nat), x = y + k → motive k) (h₂ : x < y → motive 0) :

motive (x - y)

theorem Nat.succ_sub {m n : Nat} (h : n ≤ m) :

m.succ - n = (m - n).succ

theorem Nat.sub_pos_of_lt {m n : Nat} (h : m < n) :

0 < n - m

theorem Nat.sub_sub (n m k : Nat) :

n - m - k = n - (m + k)

theorem Nat.sub_le_sub_left {n m : Nat} (h : n ≤ m) (k : Nat) :

k - m ≤ k - n

theorem Nat.sub_le_sub_right {n m : Nat} (h : n ≤ m) (k : Nat) :

n - k ≤ m - k

theorem Nat.sub_le_add_right_sub (a i j : Nat) :

a - i ≤ a + j - i

theorem Nat.lt_of_sub_ne_zero {n m : Nat} (h : n - m ≠ 0) :

m < n

theorem Nat.sub_ne_zero_iff_lt {n m : Nat} :

n - m ≠ 0 ↔ m < n

theorem Nat.lt_of_sub_pos {n m : Nat} (h : 0 < n - m) :

m < n

theorem Nat.lt_of_sub_eq_succ {m n l : Nat} (h : m - n = l.succ) :

n < m

theorem Nat.lt_of_sub_eq_sub_one {m n l : Nat} (h : m - n = l + 1) :

n < m

theorem Nat.sub_lt_left_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < n + m) :

k - n < m

theorem Nat.sub_lt_right_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < m + n) :

k - n < m

theorem Nat.le_of_sub_eq_zero {n m : Nat} :

n - m = 0 → n ≤ m

theorem Nat.le_of_sub_le_sub_right {n m k : Nat} :

k ≤ m → n - k ≤ m - k → n ≤ m

theorem Nat.sub_le_sub_iff_right {k m n : Nat} (h : k ≤ m) :

n - k ≤ m - k ↔ n ≤ m

theorem Nat.sub_eq_iff_eq_add {b a c : Nat} (h : b ≤ a) :

a - b = c ↔ a = c + b

theorem Nat.sub_eq_iff_eq_add' {b a c : Nat} (h : b ≤ a) :

a - b = c ↔ a = b + c

theorem Nat.sub_one_sub_lt_of_lt {a b : Nat} (h : a < b) :

b - 1 - a < b

Mul sub distrib #

theorem Nat.pred_mul (n m : Nat) :

n.pred * m = n * m - m

theorem Nat.sub_one_mul (n m : Nat) :

(n - 1) * m = n * m - m

theorem Nat.mul_pred (n m : Nat) :

n * m.pred = n * m - n

theorem Nat.mul_sub_one (n m : Nat) :

n * (m - 1) = n * m - n

theorem Nat.mul_sub_right_distrib (n m k : Nat) :

(n - m) * k = n * k - m * k

theorem Nat.sub_mul (n m k : Nat) :

(n - m) * k = n * k - m * k

theorem Nat.mul_sub_left_distrib (n m k : Nat) :

n * (m - k) = n * m - n * k

theorem Nat.mul_sub (n m k : Nat) :

n * (m - k) = n * m - n * k

Helper normalization theorems #

theorem Nat.not_le_eq (a b : Nat) :

(¬a ≤ b) = (b + 1 ≤ a)

theorem Nat.not_ge_eq (a b : Nat) :

(¬a ≥ b) = (a + 1 ≤ b)

theorem Nat.not_lt_eq (a b : Nat) :

(¬a < b) = (b ≤ a)

theorem Nat.not_gt_eq (a b : Nat) :

(¬a > b) = (a ≤ b)

@[csimp]

theorem Nat.repeat_eq_repeatTR :

@«repeat» = @repeatTR