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

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

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

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

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

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

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

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

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

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

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

a.blt b = a.succ.ble b

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 #

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

Nat.instTransLt = { trans := ⋯ }

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 := ⋯ }

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 := ⋯ }

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 := ⋯ }

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

n ≤ m

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

n < m → n < m.succ

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

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.instAntisymmNotLt :

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

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

@Nat.not_lt_of_gt = @Nat.lt_asymm

Instances For

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

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

@Nat.lt_iff_le_and_not_ge = @Nat.lt_iff_le_not_le

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

@Nat.lt_or_gt = @Nat.ne_iff_lt_or_gt

Instances For

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

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

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

Nat.one_pos = Nat.zero_lt_one

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.succ_le {n m : Nat} :

n.succ ≤ m ↔ n < m

theorem Nat.add_one_le_iff {n m : Nat} :

n + 1 ≤ m ↔ n < m

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

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

@[deprecated Nat.succ_inj (since := "2025-04-14")]

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

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_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_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 #

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)

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

n.min m = min n m

Instances For

theorem Nat.min_def {n m : Nat} :

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

instance Nat.instMax :

Equations

Nat.instMax = maxOfLe

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

n.max m = max n m

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