source
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

- Nat.recCompiled zero succ Nat.zero = zero
- Nat.recCompiled zero succ n.succ = succ n (Nat.recCompiled zero succ n)

Instances For

source
@[csimp]
theorem Nat.rec_eq_recCompiled :
@rec = @recCompiled
source
@[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

- Nat.recAux zero succ t = Nat.rec zero succ t

Instances For

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

- Nat.casesAuxOn t zero succ = Nat.casesOn t zero succ

Instances For

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

- Nat.repeat f 0 x✝ = x✝
- Nat.repeat f n.succ x✝ = f (Nat.repeat f n x✝)

Instances For

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

- Nat.repeatTR f n a = Nat.repeatTR.loop✝ f n a

Instances For

source
def Nat.blt (a b : Nat) :
Bool

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

- a.blt b = a.succ.ble b

Instances For

source
theorem Nat.and_forall_add_one {p : Nat → Prop} :
(p 0 ∧ ∀ (n : Nat), p (n + 1)) ↔ ∀ (n : Nat), p n
source
theorem Nat.or_exists_add_one {p : Nat → Prop} :
(p 0 ∨ ∃ (n : Nat), p (n + 1)) ↔ Exists p

# Helper "packing" theorems #

source
@[simp]
theorem Nat.zero_eq :
zero = 0
source
@[simp]
theorem Nat.add_eq {x y : Nat} :
x.add y = x + y
source
@[simp]
theorem Nat.mul_eq {x y : Nat} :
x.mul y = x * y
source
@[simp]
theorem Nat.sub_eq {x y : Nat} :
x.sub y = x - y
source
@[simp]
theorem Nat.lt_eq {x y : Nat} :
x.lt y = (x < y)
source
@[simp]
theorem Nat.le_eq {x y : Nat} :
x.le y = (x ≤ y)

# Helper Bool relation theorems #

source
@[simp]
theorem Nat.beq_refl (a : Nat) :
a.beq a = true
source
@[simp]
theorem Nat.beq_eq {x y : Nat} :
(x.beq y = true) = (x = y)
source
@[simp]
theorem Nat.ble_eq {x y : Nat} :
(x.ble y = true) = (x ≤ y)
source
@[simp]
theorem Nat.blt_eq {x y : Nat} :
(x.blt y = true) = (x < y)
source
instance Nat.instLawfulBEq :
LawfulBEq Nat
source
theorem Nat.beq_eq_true_eq (a b : Nat) :
((a == b) = true) = (a = b)
source
theorem Nat.not_beq_eq_true_eq (a b : Nat) :
((!a == b) = true) = ¬a = b

# Nat.add theorems #

source
@[simp]
theorem Nat.zero_add (n : Nat) :
0 + n = n
source
instance Nat.instLawfulIdentityHAddOfNat :
Std.LawfulIdentity (fun (x1 x2 : Nat) => x1 + x2) 0
source
theorem Nat.succ_add (n m : Nat) :
n.succ + m = (n + m).succ
source
theorem Nat.add_succ (n m : Nat) :
n + m.succ = (n + m).succ
source
theorem Nat.add_one (n : Nat) :
n + 1 = n.succ
source
@[simp]
theorem Nat.succ_eq_add_one (n : Nat) :
n.succ = n + 1
source
theorem Nat.add_one_ne_zero (n : Nat) :
n + 1 ≠ 0
source
theorem Nat.zero_ne_add_one (n : Nat) :
0 ≠ n + 1
source
theorem Nat.add_comm (n m : Nat) :
n + m = m + n
source
instance Nat.instCommutativeHAdd :
Std.Commutative fun (x1 x2 : Nat) => x1 + x2
source
theorem Nat.add_assoc (n m k : Nat) :
n + m + k = n + (m + k)
source
instance Nat.instAssociativeHAdd :
Std.Associative fun (x1 x2 : Nat) => x1 + x2
source
theorem Nat.add_left_comm (n m k : Nat) :
n + (m + k) = m + (n + k)
source
theorem Nat.add_right_comm (n m k : Nat) :
n + m + k = n + k + m
source
theorem Nat.add_left_cancel {n m k : Nat} :
n + m = n + k → m = k
source
theorem Nat.add_right_cancel {n m k : Nat} (h : n + m = k + m) :
n = k
source
theorem Nat.eq_zero_of_add_eq_zero {n m : Nat} :
n + m = 0 → n = 0 ∧ m = 0
source
theorem Nat.eq_zero_of_add_eq_zero_left {n m : Nat} (h : n + m = 0) :
m = 0

# Nat.mul theorems #

source
@[simp]
theorem Nat.mul_zero (n : Nat) :
n * 0 = 0
source
theorem Nat.mul_succ (n m : Nat) :
n * m.succ = n * m + n
source
theorem Nat.mul_add_one (n m : Nat) :
n * (m + 1) = n * m + n
source
@[simp]
theorem Nat.zero_mul (n : Nat) :
0 * n = 0
source
theorem Nat.succ_mul (n m : Nat) :
n.succ * m = n * m + m
source
theorem Nat.add_one_mul (n m : Nat) :
(n + 1) * m = n * m + m
source
theorem Nat.mul_comm (n m : Nat) :
n * m = m * n
source
instance Nat.instCommutativeHMul :
Std.Commutative fun (x1 x2 : Nat) => x1 * x2
source
@[simp]
theorem Nat.mul_one (n : Nat) :
n * 1 = n
source
@[simp]
theorem Nat.one_mul (n : Nat) :
1 * n = n
source
instance Nat.instLawfulIdentityHMulOfNat :
Std.LawfulIdentity (fun (x1 x2 : Nat) => x1 * x2) 1
source
theorem Nat.left_distrib (n m k : Nat) :
n * (m + k) = n * m + n * k
source
theorem Nat.right_distrib (n m k : Nat) :
(n + m) * k = n * k + m * k
source
theorem Nat.mul_add (n m k : Nat) :
n * (m + k) = n * m + n * k
source
theorem Nat.add_mul (n m k : Nat) :
(n + m) * k = n * k + m * k
source
theorem Nat.mul_assoc (n m k : Nat) :
n * m * k = n * (m * k)
source
instance Nat.instAssociativeHMul :
Std.Associative fun (x1 x2 : Nat) => x1 * x2
source
theorem Nat.mul_left_comm (n m k : Nat) :
n * (m * k) = m * (n * k)
source
theorem Nat.mul_two (n : Nat) :
n * 2 = n + n
source
theorem Nat.two_mul (n : Nat) :
2 * n = n + n

# Inequalities #

source
theorem Nat.succ_lt_succ {n m : Nat} :
n < m → n.succ < m.succ
source
theorem Nat.le_of_lt_add_one {n m : Nat} :
n < m + 1 → n ≤ m
source
theorem Nat.lt_add_one_of_le {n m : Nat} :
n ≤ m → n < m + 1
source
@[simp]
theorem Nat.sub_zero (n : Nat) :
n - 0 = n
source
theorem Nat.not_add_one_le_zero (n : Nat) :
¬n + 1 ≤ 0
source
theorem Nat.not_add_one_le_self (n : Nat) :
¬n + 1 ≤ n
source
theorem Nat.add_one_pos (n : Nat) :
0 < n + 1
source
theorem Nat.pred_lt {n : Nat} :
n ≠ 0 → n.pred < n
source
theorem Nat.sub_one_lt {n : Nat} :
n ≠ 0 → n - 1 < n
source
theorem Nat.sub_lt_of_lt {a b c : Nat} (h : a < c) :
a - b < c
source
theorem Nat.sub_succ (n m : Nat) :
n - m.succ = (n - m).pred
source
theorem Nat.succ_sub_succ (n m : Nat) :
n.succ - m.succ = n - m
source
@[simp]
theorem Nat.sub_self (n : Nat) :
n - n = 0
source
theorem Nat.sub_add_eq (a b c : Nat) :
a - (b + c) = a - b - c
source
theorem Nat.lt_of_lt_of_eq {n m k : Nat} :
n < m → m = k → n < k
source
instance Nat.instTransLt :
Trans (fun (x1 x2 : Nat) => x1 < x2) (fun (x1 x2 : Nat) => x1 < x2) fun (x1 x2 : Nat) => x1 < x2
Equations

- Nat.instTransLt = { trans := ⋯ }

source
instance Nat.instTransLe :
Trans (fun (x1 x2 : Nat) => x1 ≤ x2) (fun (x1 x2 : Nat) => x1 ≤ x2) fun (x1 x2 : Nat) => x1 ≤ x2
Equations

- Nat.instTransLe = { trans := ⋯ }

source
instance Nat.instTransLtLe :
Trans (fun (x1 x2 : Nat) => x1 < x2) (fun (x1 x2 : Nat) => x1 ≤ x2) fun (x1 x2 : Nat) => x1 < x2
Equations

- Nat.instTransLtLe = { trans := ⋯ }

source
instance Nat.instTransLeLt :
Trans (fun (x1 x2 : Nat) => x1 ≤ x2) (fun (x1 x2 : Nat) => x1 < x2) fun (x1 x2 : Nat) => x1 < x2
Equations

- Nat.instTransLeLt = { trans := ⋯ }

source
theorem Nat.le_of_eq {n m : Nat} (p : n = m) :
n ≤ m
source
theorem Nat.lt.step {n m : Nat} :
n < m → n < m.succ
source
theorem Nat.le_of_succ_le {n m : Nat} (h : n.succ ≤ m) :
n ≤ m
source
theorem Nat.lt_of_succ_lt {n m : Nat} :
n.succ < m → n < m
source
theorem Nat.le_of_lt {n m : Nat} :
n < m → n ≤ m
source
theorem Nat.lt_of_succ_lt_succ {n m : Nat} :
n.succ < m.succ → n < m
source
theorem Nat.lt_of_succ_le {n m : Nat} (h : n.succ ≤ m) :
n < m
source
theorem Nat.succ_le_of_lt {n m : Nat} (h : n < m) :
n.succ ≤ m
source
theorem Nat.eq_zero_or_pos (n : Nat) :
n = 0 ∨ n > 0
source
theorem Nat.pos_of_ne_zero {n : Nat} :
n ≠ 0 → 0 < n
source
theorem Nat.pos_of_neZero (n : Nat) [NeZero n] :
0 < n
source
theorem Nat.lt.base (n : Nat) :
n < n.succ
source
theorem Nat.le_total (m n : Nat) :
m ≤ n ∨ n ≤ m
source
theorem Nat.eq_zero_of_le_zero {n : Nat} (h : n ≤ 0) :
n = 0
source
theorem Nat.zero_lt_of_lt {a b : Nat} :
a < b → 0 < b
source
theorem Nat.zero_lt_of_ne_zero {a : Nat} (h : a ≠ 0) :
0 < a
source
theorem Nat.ne_of_lt {a b : Nat} (h : a < b) :
a ≠ b
source
theorem Nat.le_or_eq_of_le_succ {m n : Nat} (h : m ≤ n.succ) :
m ≤ n ∨ m = n.succ
source
theorem Nat.le_or_eq_of_le_add_one {m n : Nat} (h : m ≤ n + 1) :
m ≤ n ∨ m = n + 1
source
@[simp]
theorem Nat.le_add_right (n k : Nat) :
n ≤ n + k
source
@[simp]
theorem Nat.le_add_left (n m : Nat) :
n ≤ m + n
source
theorem Nat.le_of_add_right_le {n m k : Nat} (h : n + k ≤ m) :
n ≤ m
source
theorem Nat.le_add_right_of_le {n m k : Nat} (h : n ≤ m) :
n ≤ m + k
source
theorem Nat.le_of_add_left_le {n m k : Nat} (h : k + n ≤ m) :
n ≤ m
source
theorem Nat.le_add_left_of_le {n m k : Nat} (h : n ≤ m) :
n ≤ k + m
source
theorem Nat.lt_of_add_one_le {n m : Nat} (h : n + 1 ≤ m) :
n < m
source
theorem Nat.add_one_le_of_lt {n m : Nat} (h : n < m) :
n + 1 ≤ m
source
theorem Nat.lt_add_left {a b : Nat} (c : Nat) (h : a < b) :
a < c + b
source
theorem Nat.lt_add_right {a b : Nat} (c : Nat) (h : a < b) :
a < b + c
source
theorem Nat.lt_of_add_right_lt {n m k : Nat} (h : n + k < m) :
n < m
source
theorem Nat.lt_of_add_left_lt {n m k : Nat} (h : k + n < m) :
n < m
source
theorem Nat.le.dest {n m : Nat} :
n ≤ m → ∃ (k : Nat), n + k = m
source
theorem Nat.le.intro {n m k : Nat} (h : n + k = m) :
n ≤ m
source
theorem Nat.not_le_of_gt {n m : Nat} (h : n > m) :
¬n ≤ m
source
theorem Nat.not_le_of_lt {a b : Nat} :
a < b → ¬b ≤ a
source
theorem Nat.not_lt_of_ge {a b : Nat} :
b ≥ a → ¬b < a
source
theorem Nat.not_lt_of_le {a b : Nat} :
a ≤ b → ¬b < a
source
theorem Nat.lt_le_asymm {a b : Nat} :
a < b → ¬b ≤ a
source
theorem Nat.le_lt_asymm {a b : Nat} :
a ≤ b → ¬b < a
source
theorem Nat.gt_of_not_le {n m : Nat} (h : ¬n ≤ m) :
n > m
source
theorem Nat.lt_of_not_ge {a b : Nat} :
¬b ≥ a → b < a
source
theorem Nat.ge_of_not_lt {n m : Nat} (h : ¬n < m) :
n ≥ m
source
theorem Nat.le_of_not_gt {a b : Nat} :
¬b > a → b ≤ a
source
theorem Nat.le_of_not_lt {a b : Nat} :
¬a < b → b ≤ a
source
theorem Nat.ne_of_gt {a b : Nat} (h : b < a) :
a ≠ b
source
theorem Nat.ne_of_lt' {a b : Nat} :
a < b → b ≠ a
source
@[simp]
theorem Nat.not_le {a b : Nat} :
¬a ≤ b ↔ b < a
source
@[simp]
theorem Nat.not_lt {a b : Nat} :
¬a < b ↔ b ≤ a
source
theorem Nat.le_of_not_le {a b : Nat} (h : ¬b ≤ a) :
a ≤ b
source
theorem Nat.le_of_not_ge {a b : Nat} :
¬a ≥ b → a ≤ b
source
theorem Nat.lt_trichotomy (a b : Nat) :
a < b ∨ a = b ∨ b < a
source
theorem Nat.lt_or_gt_of_ne {a b : Nat} (ne : a ≠ b) :
a < b ∨ a > b
source
theorem Nat.lt_or_lt_of_ne {a b : Nat} :
a ≠ b → a < b ∨ b < a
source
theorem Nat.le_antisymm_iff {a b : Nat} :
a = b ↔ a ≤ b ∧ b ≤ a
source
theorem Nat.eq_iff_le_and_ge {a b : Nat} :
a = b ↔ a ≤ b ∧ b ≤ a
source
instance Nat.instAntisymmLe :
Std.Antisymm fun (x1 x2 : Nat) => x1 ≤ x2
source
instance Nat.instAntisymmNotLt :
Std.Antisymm fun (x1 x2 : Nat) => ¬x1 < x2
source
theorem Nat.add_le_add_left {n m : Nat} (h : n ≤ m) (k : Nat) :
k + n ≤ k + m
source
theorem Nat.add_le_add_right {n m : Nat} (h : n ≤ m) (k : Nat) :
n + k ≤ m + k
source
theorem Nat.add_lt_add_left {n m : Nat} (h : n < m) (k : Nat) :
k + n < k + m
source
theorem Nat.add_lt_add_right {n m : Nat} (h : n < m) (k : Nat) :
n + k < m + k
source
theorem Nat.lt_add_of_pos_left {k n : Nat} (h : 0 < k) :
n < k + n
source
theorem Nat.lt_add_of_pos_right {k n : Nat} (h : 0 < k) :
n < n + k
source
theorem Nat.zero_lt_one :
0 < 1
source
theorem Nat.pos_iff_ne_zero {n : Nat} :
0 < n ↔ n ≠ 0
source
theorem Nat.add_le_add {a b c d : Nat} (h₁ : a ≤ b) (h₂ : c ≤ d) :
a + c ≤ b + d
source
theorem Nat.add_lt_add {a b c d : Nat} (h₁ : a < b) (h₂ : c < d) :
a + c < b + d
source
theorem Nat.le_of_add_le_add_left {a b c : Nat} (h : a + b ≤ a + c) :
b ≤ c
source
theorem Nat.le_of_add_le_add_right {a b c : Nat} :
a + b ≤ c + b → a ≤ c
source
@[simp]
theorem Nat.add_le_add_iff_right {m k n : Nat} :
m + n ≤ k + n ↔ m ≤ k
source
@[simp]
theorem Nat.add_le_add_iff_left {m k n : Nat} :
n + m ≤ n + k ↔ m ≤ k

### le/lt #

source
theorem Nat.lt_asymm {a b : Nat} (h : a < b) :
¬b < a
source
@[reducible, inline]
abbrev Nat.not_lt_of_gt {a b : Nat} (h : a < b) :
¬b < a

Alias for `Nat.lt_asymm`.

Equations

- @Nat.not_lt_of_gt = @Nat.lt_asymm

Instances For

source
@[reducible, inline]
abbrev Nat.not_lt_of_lt {a b : Nat} (h : a < b) :
¬b < a

Alias for `Nat.lt_asymm`.

Equations

- @Nat.not_lt_of_lt = @Nat.lt_asymm

Instances For

source
theorem Nat.lt_iff_le_not_le {m n : Nat} :
m < n ↔ m ≤ n ∧ ¬n ≤ m
source
@[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

- @Nat.lt_iff_le_and_not_ge = @Nat.lt_iff_le_not_le

Instances For

source
theorem Nat.lt_iff_le_and_ne {m n : Nat} :
m < n ↔ m ≤ n ∧ m ≠ n
source
theorem Nat.ne_iff_lt_or_gt {a b : Nat} :
a ≠ b ↔ a < b ∨ b < a
source
@[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

- @Nat.lt_or_gt = @Nat.ne_iff_lt_or_gt

Instances For

source
@[reducible, inline]
abbrev Nat.le_or_ge (m n : Nat) :
m ≤ n ∨ n ≤ m

Alias for `Nat.le_total`.

Equations

- Nat.le_or_ge = Nat.le_total

Instances For

source
@[reducible, inline]
abbrev Nat.le_or_le (m n : Nat) :
m ≤ n ∨ n ≤ m

Alias for `Nat.le_total`.

Equations

- Nat.le_or_le = Nat.le_total

Instances For

source
theorem Nat.eq_or_lt_of_not_lt {a b : Nat} (hnlt : ¬a < b) :
a = b ∨ b < a
source
theorem Nat.lt_or_eq_of_le {n m : Nat} (h : n ≤ m) :
n < m ∨ n = m
source
theorem Nat.le_iff_lt_or_eq {n m : Nat} :
n ≤ m ↔ n < m ∨ n = m
source
theorem Nat.lt_succ_iff {m n : Nat} :
m < n.succ ↔ m ≤ n
source
theorem Nat.lt_add_one_iff {m n : Nat} :
m < n + 1 ↔ m ≤ n
source
theorem Nat.lt_succ_iff_lt_or_eq {m n : Nat} :
m < n.succ ↔ m < n ∨ m = n
source
theorem Nat.lt_add_one_iff_lt_or_eq {m n : Nat} :
m < n + 1 ↔ m < n ∨ m = n
source
theorem Nat.eq_of_lt_succ_of_not_lt {m n : Nat} (hmn : m < n + 1) (h : ¬m < n) :
m = n
source
theorem Nat.eq_of_le_of_lt_succ {n m : Nat} (h₁ : n ≤ m) (h₂ : m < n + 1) :
m = n

## zero/one/two #

source
theorem Nat.le_zero {i : Nat} :
i ≤ 0 ↔ i = 0
source
@[reducible, inline]
abbrev Nat.one_pos :
0 < 1

Alias for `Nat.zero_lt_one`.

Equations

- Nat.one_pos = Nat.zero_lt_one

Instances For

source
theorem Nat.two_pos :
0 < 2
source
theorem Nat.ne_zero_iff_zero_lt {n : Nat} :
n ≠ 0 ↔ 0 < n
source
theorem Nat.zero_lt_two :
0 < 2
source
theorem Nat.one_lt_two :
1 < 2
source
theorem Nat.eq_zero_of_not_pos {n : Nat} (h : ¬0 < n) :
n = 0

## succ/pred #

source
@[simp]
theorem Nat.succ_ne_self (n : Nat) :
n.succ ≠ n
source
theorem Nat.add_one_ne_self (n : Nat) :
n + 1 ≠ n
source
theorem Nat.succ_le {n m : Nat} :
n.succ ≤ m ↔ n < m
source
theorem Nat.add_one_le_iff {n m : Nat} :
n + 1 ≤ m ↔ n < m
source
theorem Nat.lt_succ {m n : Nat} :
m < n.succ ↔ m ≤ n
source
theorem Nat.lt_succ_of_lt {a b : Nat} (h : a < b) :
a < b.succ
source
theorem Nat.lt_add_one_of_lt {a b : Nat} (h : a < b) :
a < b + 1
source
@[simp]
theorem Nat.lt_one_iff {n : Nat} :
n < 1 ↔ n = 0
source
theorem Nat.succ_pred_eq_of_ne_zero {n : Nat} :
n ≠ 0 → n.pred.succ = n
source
theorem Nat.eq_zero_or_eq_succ_pred (n : Nat) :
n = 0 ∨ n = n.pred.succ
source
theorem Nat.succ_inj {a b : Nat} :
a.succ = b.succ ↔ a = b
source
@[deprecated Nat.succ_inj (since := "2025-04-14")]
theorem Nat.succ_inj' {a b : Nat} :
a.succ = b.succ ↔ a = b
source
theorem Nat.succ_le_succ_iff {a b : Nat} :
a.succ ≤ b.succ ↔ a ≤ b
source
theorem Nat.succ_lt_succ_iff {a b : Nat} :
a.succ < b.succ ↔ a < b
source
theorem Nat.succ_ne_succ_iff {a b : Nat} :
a.succ ≠ b.succ ↔ a ≠ b
source
theorem Nat.succ_succ_ne_one (a : Nat) :
a.succ.succ ≠ 1
source
theorem Nat.add_one_inj {a b : Nat} :
a + 1 = b + 1 ↔ a = b
source
theorem Nat.ne_add_one (n : Nat) :
n ≠ n + 1
source
theorem Nat.add_one_ne (n : Nat) :
n + 1 ≠ n
source
theorem Nat.add_one_le_add_one_iff {a b : Nat} :
a + 1 ≤ b + 1 ↔ a ≤ b
source
theorem Nat.add_one_lt_add_one_iff {a b : Nat} :
a + 1 < b + 1 ↔ a < b
source
theorem Nat.add_one_ne_add_one_iff {a b : Nat} :
a + 1 ≠ b + 1 ↔ a ≠ b
source
theorem Nat.add_one_add_one_ne_one {a : Nat} :
a + 1 + 1 ≠ 1
source
theorem Nat.pred_inj {a b : Nat} :
0 < a → 0 < b → a.pred = b.pred → a = b
source
theorem Nat.pred_ne_self {a : Nat} :
a ≠ 0 → a.pred ≠ a
source
theorem Nat.sub_one_ne_self {a : Nat} :
a ≠ 0 → a - 1 ≠ a
source
theorem Nat.pred_lt_self {a : Nat} :
0 < a → a.pred < a
source
theorem Nat.pred_lt_pred {n m : Nat} :
n ≠ 0 → n < m → n.pred < m.pred
source
theorem Nat.pred_le_iff_le_succ {n : Nat} {m : Nat} :
n.pred ≤ m ↔ n ≤ m.succ
source
theorem Nat.le_succ_of_pred_le {n : Nat} {m : Nat} :
n.pred ≤ m → n ≤ m.succ
source
theorem Nat.pred_le_of_le_succ {n m : Nat} :
n ≤ m.succ → n.pred ≤ m
source
theorem Nat.lt_pred_iff_succ_lt {n : Nat} {m : Nat} :
n < m.pred ↔ n.succ < m
source
theorem Nat.succ_lt_of_lt_pred {n : Nat} {m : Nat} :
n < m.pred → n.succ < m
source
theorem Nat.lt_pred_of_succ_lt {n m : Nat} :
n.succ < m → n < m.pred
source
theorem Nat.le_pred_iff_lt {n : Nat} {m : Nat} :
0 < m → (n ≤ m.pred ↔ n < m)
source
theorem Nat.le_pred_of_lt {n m : Nat} (h : n < m) :
n ≤ m.pred
source
theorem Nat.le_sub_one_of_lt {a b : Nat} :
a < b → a ≤ b - 1
source
theorem Nat.lt_of_le_pred {m : Nat} {n : Nat} (h : 0 < m) :
n ≤ m.pred → n < m
source
theorem Nat.lt_of_le_sub_one {m n : Nat} (h : 0 < m) :
n ≤ m - 1 → n < m
source
theorem Nat.le_sub_one_iff_lt {m n : Nat} (h : 0 < m) :
n ≤ m - 1 ↔ n < m
source
theorem Nat.exists_eq_succ_of_ne_zero {n : Nat} :
n ≠ 0 → ∃ (k : Nat), n = k.succ
source
theorem Nat.exists_eq_add_one_of_ne_zero {n : Nat} :
n ≠ 0 → ∃ (k : Nat), n = k + 1

# Basic theorems for comparing numerals #

source
theorem Nat.ctor_eq_zero :
zero = 0
source
theorem Nat.one_ne_zero :
1 ≠ 0
source
@[simp]
theorem Nat.zero_ne_one :
0 ≠ 1
source
theorem Nat.succ_ne_zero (n : Nat) :
n.succ ≠ 0
source
instance Nat.instNeZeroSucc {n : Nat} :
NeZero (n + 1)
source
@[simp]
theorem Nat.default_eq_zero :
default = 0

# mul + order #

source
theorem Nat.mul_le_mul_left {n m : Nat} (k : Nat) (h : n ≤ m) :
k * n ≤ k * m
source
theorem Nat.mul_le_mul_right {n m : Nat} (k : Nat) (h : n ≤ m) :
n * k ≤ m * k
source
theorem Nat.mul_le_mul {n₁ m₁ n₂ m₂ : Nat} (h₁ : n₁ ≤ n₂) (h₂ : m₁ ≤ m₂) :
n₁ * m₁ ≤ n₂ * m₂
source
theorem Nat.mul_lt_mul_of_pos_left {n m k : Nat} (h : n < m) (hk : k > 0) :
k * n < k * m
source
theorem Nat.mul_lt_mul_of_pos_right {n m k : Nat} (h : n < m) (hk : k > 0) :
n * k < m * k
source
theorem Nat.le_of_mul_le_mul_left {a b c : Nat} (h : c * a ≤ c * b) (hc : 0 < c) :
a ≤ b
source
theorem Nat.le_of_mul_le_mul_right {a b c : Nat} (h : a * c ≤ b * c) (hc : 0 < c) :
a ≤ b
source
theorem Nat.mul_le_mul_left_iff {n m k : Nat} (w : 0 < k) :
k * n ≤ k * m ↔ n ≤ m
source
theorem Nat.mul_le_mul_right_iff {n m k : Nat} (w : 0 < k) :
n * k ≤ m * k ↔ n ≤ m
source
theorem Nat.eq_of_mul_eq_mul_left {m k n : Nat} (hn : 0 < n) (h : n * m = n * k) :
m = k
source
theorem Nat.eq_of_mul_eq_mul_right {n m k : Nat} (hm : 0 < m) (h : n * m = k * m) :
n = k

# power #

source
theorem Nat.pow_succ (n m : Nat) :
n ^ m.succ = n ^ m * n
source
theorem Nat.pow_add_one (n m : Nat) :
n ^ (m + 1) = n ^ m * n
source
@[simp]
theorem Nat.pow_zero (n : Nat) :
n ^ 0 = 1
source
@[simp]
theorem Nat.pow_one (a : Nat) :
a ^ 1 = a
source
theorem Nat.pow_le_pow_left {n m : Nat} (h : n ≤ m) (i : Nat) :
n ^ i ≤ m ^ i
source
theorem Nat.pow_le_pow_right {n : Nat} (hx : n > 0) {i j : Nat} :
i ≤ j → n ^ i ≤ n ^ j
source
@[simp]
theorem Nat.zero_pow_of_pos (n : Nat) (h : 0 < n) :
0 ^ n = 0
source
theorem Nat.two_pow_pos (w : Nat) :
0 < 2 ^ w
source
instance Nat.instNeZeroHPow {n m : Nat} [NeZero n] :
NeZero (n ^ m)
source
theorem Nat.mul_pow (a b n : Nat) :
(a * b) ^ n = a ^ n * b ^ n
source
theorem Nat.pow_lt_pow_left {a b n : Nat} (hab : a < b) (h : n ≠ 0) :
a ^ n < b ^ n
source
theorem Nat.pow_left_inj {a b n : Nat} (hn : n ≠ 0) :
a ^ n = b ^ n ↔ a = b

# min/max #

source
@[reducible, inline]
abbrev Nat.min (n m : Nat) :
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

- n.min m = min n m

Instances For

source
theorem Nat.min_def {n m : Nat} :
min n m = if n ≤ m then n else m
source
instance Nat.instMax :
Max Nat
Equations

- Nat.instMax = maxOfLe

source
@[reducible, inline]
abbrev Nat.max (n m : Nat) :
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

- n.max m = max n m

Instances For

source
theorem Nat.max_def {n m : Nat} :
max n m = if n ≤ m then m else n

# Auxiliary theorems for well-founded recursion #

source
theorem Nat.ne_zero_of_lt {b a : Nat} (h : b < a) :
a ≠ 0
source
theorem Nat.pred_lt_of_lt {n m : Nat} (h : m < n) :
n.pred < n
source
theorem Nat.sub_one_lt_of_lt {n m : Nat} (h : m < n) :
n - 1 < n

# pred theorems #

source
theorem Nat.pred_zero :
pred 0 = 0
source
theorem Nat.pred_succ (n : Nat) :
n.succ.pred = n
source
@[simp]
theorem Nat.zero_sub_one :
0 - 1 = 0
source
@[simp]
theorem Nat.add_one_sub_one (n : Nat) :
n + 1 - 1 = n
source
theorem Nat.sub_one_eq_self {n : Nat} :
n - 1 = n ↔ n = 0
source
theorem Nat.eq_self_sub_one {n : Nat} :
n = n - 1 ↔ n = 0
source
theorem Nat.succ_pred {a : Nat} (h : a ≠ 0) :
a.pred.succ = a
source
theorem Nat.sub_one_add_one {a : Nat} (h : a ≠ 0) :
a - 1 + 1 = a
source
theorem Nat.succ_pred_eq_of_pos {n : Nat} :
0 < n → n.pred.succ = n
source
theorem Nat.sub_one_add_one_eq_of_pos {n : Nat} :
0 < n → n - 1 + 1 = n
source
theorem Nat.eq_zero_or_eq_sub_one_add_one {n : Nat} :
n = 0 ∨ n = n - 1 + 1
source
@[simp]
theorem Nat.pred_eq_sub_one {n : Nat} :
n.pred = n - 1

# sub theorems #

source
theorem Nat.add_sub_self_left (a b : Nat) :
a + b - a = b
source
theorem Nat.add_sub_self_right (a b : Nat) :
a + b - b = a
source
theorem Nat.sub_le_succ_sub (a i : Nat) :
a - i ≤ a.succ - i
source
theorem Nat.zero_lt_sub_of_lt {i a : Nat} (h : i < a) :
0 < a - i
source
theorem Nat.sub_succ_lt_self (a i : Nat) (h : i < a) :
a - (i + 1) < a - i
source
theorem Nat.sub_ne_zero_of_lt {a b : Nat} :
a < b → b - a ≠ 0
source
theorem Nat.add_sub_of_le {a b : Nat} (h : a ≤ b) :
a + (b - a) = b
source
theorem Nat.sub_one_cancel {a b : Nat} :
0 < a → 0 < b → a - 1 = b - 1 → a = b
source
@[simp]
theorem Nat.sub_add_cancel {n m : Nat} (h : m ≤ n) :
n - m + m = n
source
theorem Nat.add_sub_add_right (n k m : Nat) :
n + k - (m + k) = n - m
source
theorem Nat.add_sub_add_left (k n m : Nat) :
k + n - (k + m) = n - m
source
@[simp]
theorem Nat.add_sub_cancel (n m : Nat) :
n + m - m = n
source
@[simp]
theorem Nat.add_sub_cancel_left (n m : Nat) :
n + m - n = m
source
theorem Nat.add_sub_assoc {m k : Nat} (h : k ≤ m) (n : Nat) :
n + m - k = n + (m - k)
source
theorem Nat.eq_add_of_sub_eq {a b c : Nat} (hle : b ≤ a) (h : a - b = c) :
a = c + b
source
theorem Nat.sub_eq_of_eq_add {a b c : Nat} (h : a = c + b) :
a - b = c
source
theorem Nat.le_add_of_sub_le {a b c : Nat} (h : a - b ≤ c) :
a ≤ c + b
source
theorem Nat.sub_lt_sub_left {k m n : Nat} :
k < m → k < n → m - n < m - k
source
@[simp]
theorem Nat.zero_sub (n : Nat) :
0 - n = 0
source
theorem Nat.sub_lt_sub_right {a b c : Nat} :
c ≤ a → a < b → a - c < b - c
source
theorem Nat.sub_self_add (n m : Nat) :
n - (n + m) = 0
source
@[simp]
theorem Nat.sub_eq_zero_of_le {n m : Nat} (h : n ≤ m) :
n - m = 0
source
theorem Nat.sub_le_of_le_add {a b c : Nat} (h : a ≤ c + b) :
a - b ≤ c
source
theorem Nat.add_le_of_le_sub {a b c : Nat} (hle : b ≤ c) (h : a ≤ c - b) :
a + b ≤ c
source
theorem Nat.le_sub_of_add_le {a b c : Nat} (h : a + b ≤ c) :
a ≤ c - b
source
theorem Nat.add_lt_of_lt_sub {a b c : Nat} (h : a < c - b) :
a + b < c
source
theorem Nat.lt_sub_of_add_lt {a b c : Nat} (h : a + b < c) :
a < c - b
source
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)
source
theorem Nat.succ_sub {m n : Nat} (h : n ≤ m) :
m.succ - n = (m - n).succ
source
theorem Nat.sub_pos_of_lt {m n : Nat} (h : m < n) :
0 < n - m
source
theorem Nat.sub_sub (n m k : Nat) :
n - m - k = n - (m + k)
source
theorem Nat.sub_le_sub_left {n m : Nat} (h : n ≤ m) (k : Nat) :
k - m ≤ k - n
source
theorem Nat.sub_le_sub_right {n m : Nat} (h : n ≤ m) (k : Nat) :
n - k ≤ m - k
source
theorem Nat.sub_le_add_right_sub (a i j : Nat) :
a - i ≤ a + j - i
source
theorem Nat.lt_of_sub_ne_zero {n m : Nat} (h : n - m ≠ 0) :
m < n
source
theorem Nat.sub_ne_zero_iff_lt {n m : Nat} :
n - m ≠ 0 ↔ m < n
source
theorem Nat.lt_of_sub_pos {n m : Nat} (h : 0 < n - m) :
m < n
source
theorem Nat.lt_of_sub_eq_succ {m n l : Nat} (h : m - n = l.succ) :
n < m
source
theorem Nat.lt_of_sub_eq_sub_one {m n l : Nat} (h : m - n = l + 1) :
n < m
source
theorem Nat.sub_lt_left_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < n + m) :
k - n < m
source
theorem Nat.sub_lt_right_of_lt_add {n k m : Nat} (H : n ≤ k) (h : k < m + n) :
k - n < m
source
theorem Nat.le_of_sub_eq_zero {n m : Nat} :
n - m = 0 → n ≤ m
source
theorem Nat.le_of_sub_le_sub_right {n m k : Nat} :
k ≤ m → n - k ≤ m - k → n ≤ m
source
theorem Nat.sub_le_sub_iff_right {k m n : Nat} (h : k ≤ m) :
n - k ≤ m - k ↔ n ≤ m
source
theorem Nat.sub_eq_iff_eq_add {b a c : Nat} (h : b ≤ a) :
a - b = c ↔ a = c + b
source
theorem Nat.sub_eq_iff_eq_add' {b a c : Nat} (h : b ≤ a) :
a - b = c ↔ a = b + c
source
theorem Nat.sub_one_sub_lt_of_lt {a b : Nat} (h : a < b) :
b - 1 - a < b

## Mul sub distrib #

source
theorem Nat.pred_mul (n m : Nat) :
n.pred * m = n * m - m
source
theorem Nat.sub_one_mul (n m : Nat) :
(n - 1) * m = n * m - m
source
theorem Nat.mul_pred (n m : Nat) :
n * m.pred = n * m - n
source
theorem Nat.mul_sub_one (n m : Nat) :
n * (m - 1) = n * m - n
source
theorem Nat.mul_sub_right_distrib (n m k : Nat) :
(n - m) * k = n * k - m * k
source
theorem Nat.sub_mul (n m k : Nat) :
(n - m) * k = n * k - m * k
source
theorem Nat.mul_sub_left_distrib (n m k : Nat) :
n * (m - k) = n * m - n * k
source
theorem Nat.mul_sub (n m k : Nat) :
n * (m - k) = n * m - n * k

# Helper normalization theorems #

source
theorem Nat.not_le_eq (a b : Nat) :
(¬a ≤ b) = (b + 1 ≤ a)
source
theorem Nat.not_ge_eq (a b : Nat) :
(¬a ≥ b) = (a + 1 ≤ b)
source
theorem Nat.not_lt_eq (a b : Nat) :
(¬a < b) = (b ≤ a)
source
theorem Nat.not_gt_eq (a b : Nat) :
(¬a > b) = (a ≤ b)
source
@[csimp]
theorem Nat.repeat_eq_repeatTR :
@«repeat» = @repeatTR