Documentation

Init.Data.Nat.Basic

@[reducible, inline]

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

motive t

Recursor identical to Nat.rec but uses notations 0 for Nat.zero and · + 1 for Nat.succ. Used as the default Nat eliminator by the induction tactic.

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

Recursor identical to Nat.casesOn but uses notations 0 for Nat.zero and · + 1 for Nat.succ. Used as the default Nat eliminator by the cases tactic.

Equations

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

Instances For

@[specialize #[]]

def Nat.fold {α : Type u} (f : Nat → α → α) (n : Nat) (init : α) :

α

Nat.fold evaluates f on the numbers up to n exclusive, in increasing order:

Nat.fold f 3 init = init |> f 0 |> f 1 |> f 2

Equations

Nat.fold f 0 x = x
Nat.fold f n.succ x = f n (Nat.fold f n x)

Instances For

@[inline]

def Nat.foldTR {α : Type u} (f : Nat → α → α) (n : Nat) (init : α) :

α

Tail-recursive version of Nat.fold.

Equations

Nat.foldTR f n init = Nat.foldTR.loop f n n init

Instances For

@[specialize #[]]

def Nat.foldTR.loop {α : Type u} (f : Nat → α → α) (n : Nat) :

Nat → α → α

Equations

Nat.foldTR.loop f n 0 x = x
Nat.foldTR.loop f n n_1.succ x = Nat.foldTR.loop f n n_1 (f (n - n_1.succ) x)

Instances For

@[specialize #[]]

def Nat.foldRev {α : Type u} (f : Nat → α → α) (n : Nat) (init : α) :

α

Nat.foldRev evaluates f on the numbers up to n exclusive, in decreasing order:

Nat.foldRev f 3 init = f 0 <| f 1 <| f 2 <| init

Equations

Nat.foldRev f 0 x = x
Nat.foldRev f n.succ x = Nat.foldRev f n (f n x)

Instances For

@[specialize #[]]

def Nat.any (f : Nat → Bool) :

any f n = true iff there is i in [0, n-1] s.t. f i = true

Equations

Nat.any f 0 = false
Nat.any f n.succ = (Nat.any f n || f n)

Instances For

@[inline]

def Nat.anyTR (f : Nat → Bool) (n : Nat) :

Tail-recursive version of Nat.any.

Equations

Nat.anyTR f n = Nat.anyTR.loop f n n

Instances For

@[specialize #[]]

def Nat.anyTR.loop (f : Nat → Bool) (n : Nat) :

Equations

Nat.anyTR.loop f n 0 = false
Nat.anyTR.loop f n n_1.succ = (f (n - n_1.succ) || Nat.anyTR.loop f n n_1)

Instances For

@[specialize #[]]

def Nat.all (f : Nat → Bool) :

all f n = true iff every i in [0, n-1] satisfies f i = true

Equations

Nat.all f 0 = true
Nat.all f n.succ = (Nat.all f n && f n)

Instances For

@[inline]

def Nat.allTR (f : Nat → Bool) (n : Nat) :

Tail-recursive version of Nat.all.

Equations

Nat.allTR f n = Nat.allTR.loop f n n

Instances For

@[specialize #[]]

def Nat.allTR.loop (f : Nat → Bool) (n : Nat) :

Equations

Nat.allTR.loop f n 0 = true
Nat.allTR.loop f n n_1.succ = (f (n - n_1.succ) && Nat.allTR.loop f n n_1)

Instances For

@[specialize #[]]

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

α

Nat.repeat f n a is f^(n) a; that is, it iterates f n times on a.

Nat.repeat f 3 a = f <| f <| f <| a

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

α

Tail-recursive version of Nat.repeat.

Equations

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

Instances For

@[specialize #[]]

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

Nat → α → α

Equations

Nat.repeatTR.loop f 0 x = x
Nat.repeatTR.loop f n.succ x = Nat.repeatTR.loop f n (f x)

Instances For

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

Boolean less-than of natural numbers.

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 : Nat} {y : Nat} :

x.add y = x + y

@[simp]

theorem Nat.mul_eq {x : Nat} {y : Nat} :

x.mul y = x * y

@[simp]

theorem Nat.sub_eq {x : Nat} {y : Nat} :

x.sub y = x - y

@[simp]

theorem Nat.lt_eq {x : Nat} {y : Nat} :

x.lt y = (x < y)

@[simp]

theorem Nat.le_eq {x : Nat} {y : Nat} :

x.le y = (x ≤ y)

Helper Bool relation theorems #

@[simp]

theorem Nat.beq_refl (a : Nat) :

a.beq a = true

@[simp]

theorem Nat.beq_eq {x : Nat} {y : Nat} :

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

@[simp]

theorem Nat.ble_eq {x : Nat} {y : Nat} :

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

@[simp]

theorem Nat.blt_eq {x : Nat} {y : Nat} :

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

instance Nat.instLawfulBEq :

Equations

Nat.instLawfulBEq = ⋯

theorem Nat.beq_eq_true_eq (a : Nat) (b : Nat) :

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

theorem Nat.not_beq_eq_true_eq (a : Nat) (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

Equations

Nat.instLawfulIdentityHAddOfNat = ⋯

theorem Nat.succ_add (n : Nat) (m : Nat) :

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

theorem Nat.add_succ (n : Nat) (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

@[simp]

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 : Nat) (m : Nat) :

n + m = m + n

instance Nat.instCommutativeHAdd :

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

Equations

Nat.instCommutativeHAdd = ⋯

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

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

instance Nat.instAssociativeHAdd :

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

Equations

Nat.instAssociativeHAdd = ⋯

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

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

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

n + m + k = n + k + m

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

n + m = n + k → m = k

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

n = k

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

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

theorem Nat.eq_zero_of_add_eq_zero_left {n : Nat} {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 : Nat) (m : Nat) :

n * m.succ = n * m + n

theorem Nat.mul_add_one (n : Nat) (m : Nat) :

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

@[simp]

theorem Nat.zero_mul (n : Nat) :

0 * n = 0

theorem Nat.succ_mul (n : Nat) (m : Nat) :

n.succ * m = n * m + m

theorem Nat.add_one_mul (n : Nat) (m : Nat) :

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

theorem Nat.mul_comm (n : Nat) (m : Nat) :

n * m = m * n

instance Nat.instCommutativeHMul :

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

Equations

Nat.instCommutativeHMul = ⋯

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

Equations

Nat.instLawfulIdentityHMulOfNat = ⋯

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

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

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

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

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

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

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

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

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

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

instance Nat.instAssociativeHMul :

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

Equations

Nat.instAssociativeHMul = ⋯

theorem Nat.mul_left_comm (n : Nat) (m : Nat) (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 : Nat} {m : Nat} :

n < m → n.succ < m.succ

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

n ≤ m → n < m.succ

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

n < m + 1 → n ≤ m

theorem Nat.lt_add_one_of_le {n : Nat} {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.succ_sub_succ_eq_sub (n : Nat) (m : Nat) :

n.succ - m.succ = n - m

theorem Nat.pred_le (n : Nat) :

n.pred ≤ n

theorem Nat.pred_lt {n : Nat} :

n ≠ 0 → n.pred < n

theorem Nat.sub_one_lt {n : Nat} :

n ≠ 0 → n - 1 < n

@[simp]

theorem Nat.sub_le (n : Nat) (m : Nat) :

n - m ≤ n

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

0 < n → 0 < m → n - m < n

theorem Nat.sub_succ (n : Nat) (m : Nat) :

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

theorem Nat.succ_sub_succ (n : Nat) (m : Nat) :

n.succ - m.succ = n - m

@[simp]

theorem Nat.sub_self (n : Nat) :

n - n = 0

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

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

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

n < m → m ≤ k → n < k

theorem Nat.lt_of_lt_of_eq {n : Nat} {m : Nat} {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 : Nat} {m : Nat} (p : n = m) :

n ≤ m

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

n < m → n < m.succ

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

n ≤ m

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

n.succ < m → n < m

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

n < m → n ≤ m

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

n.succ < m.succ → n < m

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

n < m

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

n.succ ≤ 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.lt_succ_self (n : Nat) :

n < n.succ

@[simp]

theorem Nat.lt_add_one (n : Nat) :

n < n + 1

theorem Nat.le_total (m : Nat) (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 : Nat} {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 : Nat} {b : Nat} (h : a < b) :

a ≠ b

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

m ≤ n ∨ m = n.succ

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

m ≤ n ∨ m = n + 1

@[simp]

theorem Nat.le_add_right (n : Nat) (k : Nat) :

n ≤ n + k

@[simp]

theorem Nat.le_add_left (n : Nat) (m : Nat) :

n ≤ m + n

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

n ≤ m

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

n ≤ m + k

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

n < m

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

n + 1 ≤ m

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

a < c + b

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

a < b + c

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

n < m

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

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

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

n ≤ m

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

theorem Nat.not_le_of_lt {a : Nat} {b : Nat} :

a < b → ¬b ≤ a

theorem Nat.not_lt_of_ge {a : Nat} {b : Nat} :

b ≥ a → ¬b < a

theorem Nat.not_lt_of_le {a : Nat} {b : Nat} :

a ≤ b → ¬b < a

theorem Nat.lt_le_asymm {a : Nat} {b : Nat} :

a < b → ¬b ≤ a

theorem Nat.le_lt_asymm {a : Nat} {b : Nat} :

a ≤ b → ¬b < a

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

n > m

theorem Nat.lt_of_not_ge {a : Nat} {b : Nat} :

¬b ≥ a → b < a

theorem Nat.lt_of_not_le {a : Nat} {b : Nat} :

¬a ≤ b → b < a

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

n ≥ m

theorem Nat.le_of_not_gt {a : Nat} {b : Nat} :

¬b > a → b ≤ a

theorem Nat.le_of_not_lt {a : Nat} {b : Nat} :

¬a < b → b ≤ a

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

a ≠ b

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

a < b → b ≠ a

@[simp]

theorem Nat.not_le {a : Nat} {b : Nat} :

¬a ≤ b ↔ b < a

@[simp]

theorem Nat.not_lt {a : Nat} {b : Nat} :

¬a < b ↔ b ≤ a

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

a ≤ b

theorem Nat.le_of_not_ge {a : Nat} {b : Nat} :

¬a ≥ b → a ≤ b

theorem Nat.lt_trichotomy (a : Nat) (b : Nat) :

a < b ∨ a = b ∨ b < a

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

a < b ∨ a > b

theorem Nat.lt_or_lt_of_ne {a : Nat} {b : Nat} :

a ≠ b → a < b ∨ b < a

theorem Nat.le_antisymm_iff {a : Nat} {b : Nat} :

a = b ↔ a ≤ b ∧ b ≤ a

theorem Nat.eq_iff_le_and_ge {a : Nat} {b : Nat} :

a = b ↔ a ≤ b ∧ b ≤ a

instance Nat.instAntisymmLe :

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

Equations

Nat.instAntisymmLe = ⋯

instance Nat.instAntisymmNotLt :

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

Equations

Nat.instAntisymmNotLt = ⋯

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

k + n ≤ k + m

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

n + k ≤ m + k

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

k + n < k + m

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

n + k < m + k

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

n < k + n

theorem Nat.lt_add_of_pos_right {k : Nat} {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 : Nat} {b : Nat} {c : Nat} {d : Nat} (h₁ : a ≤ b) (h₂ : c ≤ d) :

a + c ≤ b + d

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

a + c < b + d

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

b ≤ c

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

a + b ≤ c + b → a ≤ c

@[simp]

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

m + n ≤ k + n ↔ m ≤ k

le/lt #

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

¬b < a

@[reducible, inline]

abbrev Nat.not_lt_of_gt {a : Nat} {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 : Nat} {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 : Nat} {n : Nat} :

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

@[reducible, inline]

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

m < n ↔ m ≤ n ∧ m ≠ n

theorem Nat.ne_iff_lt_or_gt {a : Nat} {b : Nat} :

a ≠ b ↔ a < b ∨ b < a

@[reducible, inline]

abbrev Nat.lt_or_gt {a : Nat} {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 : Nat) (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 : Nat) (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 : Nat} {b : Nat} (hnlt : ¬a < b) :

a = b ∨ b < a

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

n < m ∨ n = m

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

n ≤ m ↔ n < m ∨ n = m

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

m < n.succ ↔ m ≤ n

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

m < n + 1 ↔ m ≤ n

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

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

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

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

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

m = n

theorem Nat.eq_of_le_of_lt_succ {n : Nat} {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 #

theorem Nat.succ_ne_self (n : Nat) :

n.succ ≠ n

theorem Nat.add_one_ne_self (n : Nat) :

n + 1 ≠ n

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

n.succ ≤ m ↔ n < m

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

n + 1 ≤ m ↔ n < m

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

m < n.succ ↔ m ≤ n

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

a < b.succ

theorem Nat.lt_add_one_of_lt {a : Nat} {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 : Nat} {b : Nat} :

a.succ = b.succ ↔ a = b

theorem Nat.succ_le_succ_iff {a : Nat} {b : Nat} :

a.succ ≤ b.succ ↔ a ≤ b

theorem Nat.succ_lt_succ_iff {a : Nat} {b : Nat} :

a.succ < b.succ ↔ a < b

theorem Nat.add_one_inj {a : Nat} {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 : Nat} {b : Nat} :

a + 1 ≤ b + 1 ↔ a ≤ b

theorem Nat.add_one_lt_add_one_iff {a : Nat} {b : Nat} :

a + 1 < b + 1 ↔ a < b

theorem Nat.pred_inj {a : Nat} {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 : Nat} {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 : Nat} {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 : Nat} {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 : Nat} {m : Nat} (h : n < m) :

n ≤ m.pred

theorem Nat.le_sub_one_of_lt {a : Nat} {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 : Nat} {n : Nat} (h : 0 < m) :

n ≤ m - 1 → n < m

theorem Nat.le_sub_one_iff_lt {m : Nat} {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

theorem Nat.zero_ne_one :

0 ≠ 1

theorem Nat.succ_ne_zero (n : Nat) :

n.succ ≠ 0

instance Nat.instNeZeroSucc {n : Nat} :

NeZero (n + 1)

Equations

⋯ = ⋯

mul + order #

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

k * n ≤ k * m

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

n * k ≤ m * k

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

n₁ * m₁ ≤ n₂ * m₂

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

k * n < k * m

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

n * k < m * k

theorem Nat.mul_pos {n : Nat} {m : Nat} (ha : n > 0) (hb : m > 0) :

n * m > 0

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

a ≤ b

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

m = k

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

n = k

power #

theorem Nat.pow_succ (n : Nat) (m : Nat) :

n ^ m.succ = n ^ m * n

theorem Nat.pow_add_one (n : Nat) (m : Nat) :

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

@[simp]

theorem Nat.pow_zero (n : Nat) :

n ^ 0 = 1

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

n ^ i ≤ m ^ i

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

i ≤ j → n ^ i ≤ n ^ j

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

0 < n ^ m

@[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 : Nat} {m : Nat} [NeZero n] :

NeZero (n ^ m)

Equations

⋯ = ⋯

min/max #

@[reducible, inline]

abbrev Nat.min (n : Nat) (m : Nat) :

Nat.min a b is the minimum of a and b:

if a ≤ b then Nat.min a b = a
if b ≤ a then Nat.min a b = b

Equations

n.min m = min n m

Instances For

theorem Nat.min_def {n : Nat} {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 : Nat) (m : Nat) :

Nat.max a b is the maximum of a and b:

if a ≤ b then Nat.max a b = b
if b ≤ a then Nat.max a b = a

Equations

n.max m = max n m

Instances For

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

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

Auxiliary theorems for well-founded recursion #

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

a ≠ 0

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

n.pred < n

@[reducible, inline, deprecated]

abbrev Nat.pred_lt' {n : Nat} {m : Nat} (h : m < n) :

n.pred < n

Equations

@Nat.pred_lt' = @Nat.pred_lt_of_lt

Instances For

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

n - 1 < n

pred theorems #

theorem Nat.pred_zero :

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 : Nat) (b : Nat) :

a + b - a = b

theorem Nat.add_sub_self_right (a : Nat) (b : Nat) :

a + b - b = a

theorem Nat.sub_le_succ_sub (a : Nat) (i : Nat) :

a - i ≤ a.succ - i

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

0 < a - i

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

a - (i + 1) < a - i

theorem Nat.sub_ne_zero_of_lt {a : Nat} {b : Nat} :

a < b → b - a ≠ 0

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

a + (b - a) = b

theorem Nat.sub_one_cancel {a : Nat} {b : Nat} :

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

@[simp]

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

n - m + m = n

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

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

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

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

@[simp]

theorem Nat.add_sub_cancel (n : Nat) (m : Nat) :

n + m - m = n

theorem Nat.add_sub_cancel_left (n : Nat) (m : Nat) :

n + m - n = m

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

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

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

a = c + b

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

a - b = c

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

a ≤ c + b

theorem Nat.sub_lt_sub_left {k : Nat} {m : Nat} {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 : Nat} {b : Nat} {c : Nat} :

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

theorem Nat.sub_self_add (n : Nat) (m : Nat) :

n - (n + m) = 0

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

n - m = 0

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

a - b ≤ c

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

a + b ≤ c

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

a ≤ c - b

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

a + b < c

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

a < c - b

theorem Nat.sub.elim {motive : Nat → Prop} (x : Nat) (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 : Nat} {n : Nat} (h : n ≤ m) :

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

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

0 < n - m

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

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

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

k - m ≤ k - n

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

n - k ≤ m - k

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

a - i ≤ a + j - i

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

m < n

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

n - m ≠ 0 ↔ m < n

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

m < n

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

n < m

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

n < m

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

k - n < m

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

k - n < m

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

n - m = 0 → n ≤ m

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

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

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

n - k ≤ m - k ↔ n ≤ m

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

a - b = c ↔ a = c + b

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

a - b = c ↔ a = b + c

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

b - 1 - a < b

Mul sub distrib #

theorem Nat.pred_mul (n : Nat) (m : Nat) :

n.pred * m = n * m - m

@[reducible, inline, deprecated]

abbrev Nat.mul_pred_left (n : Nat) (m : Nat) :

n.pred * m = n * m - m

Equations

Nat.mul_pred_left = Nat.pred_mul

Instances For

theorem Nat.sub_one_mul (n : Nat) (m : Nat) :

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

theorem Nat.mul_pred (n : Nat) (m : Nat) :

n * m.pred = n * m - n

@[reducible, inline, deprecated]

abbrev Nat.mul_pred_right (n : Nat) (m : Nat) :

n * m.pred = n * m - n

Equations

Nat.mul_pred_right = Nat.mul_pred

Instances For

theorem Nat.mul_sub_one (n : Nat) (m : Nat) :

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

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

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

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

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

Helper normalization theorems #

theorem Nat.not_le_eq (a : Nat) (b : Nat) :

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

theorem Nat.not_ge_eq (a : Nat) (b : Nat) :

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

theorem Nat.not_lt_eq (a : Nat) (b : Nat) :

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

theorem Nat.not_gt_eq (a : Nat) (b : Nat) :

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

csimp theorems #

@[csimp]

theorem Nat.fold_eq_foldTR :

@Nat.fold = @Nat.foldTR

theorem Nat.fold_eq_foldTR.go (α : Type u_1) (f : Nat → α → α) (init : α) (m : Nat) (n : Nat) :

Nat.foldTR.loop f (m + n) m (Nat.fold f n init) = Nat.fold f (m + n) init

@[csimp]

theorem Nat.any_eq_anyTR :

Nat.any = Nat.anyTR

theorem Nat.any_eq_anyTR.go (f : Nat → Bool) (m : Nat) (n : Nat) :

(Nat.any f n || Nat.anyTR.loop f (m + n) m) = Nat.any f (m + n)

@[csimp]

theorem Nat.all_eq_allTR :

Nat.all = Nat.allTR

theorem Nat.all_eq_allTR.go (f : Nat → Bool) (m : Nat) (n : Nat) :

(Nat.all f n && Nat.allTR.loop f (m + n) m) = Nat.all f (m + n)

@[csimp]

theorem Nat.repeat_eq_repeatTR :

@Nat.repeat = @Nat.repeatTR

theorem Nat.repeat_eq_repeatTR.go (α : Type u_1) (f : α → α) (init : α) (m : Nat) (n : Nat) :

Nat.repeatTR.loop f m (Nat.repeat f n init) = Nat.repeat f (m + n) init

@[inline]

def Prod.foldI {α : Type u} (f : Nat → α → α) (i : Nat × Nat) (a : α) :

α

(start, stop).foldI f a evaluates f on all the numbers from start (inclusive) to stop (exclusive) in increasing order:

(5, 8).foldI f init = init |> f 5 |> f 6 |> f 7

Equations

Prod.foldI f i a = Nat.foldTR.loop f i.snd (i.snd - i.fst) a

Instances For

@[inline]

def Prod.anyI (f : Nat → Bool) (i : Nat × Nat) :

(start, stop).anyI f a returns true if f is true for some natural number from start (inclusive) to stop (exclusive):

(5, 8).anyI f = f 5 || f 6 || f 7

Equations

Prod.anyI f i = Nat.anyTR.loop f i.snd (i.snd - i.fst)

Instances For

@[inline]

def Prod.allI (f : Nat → Bool) (i : Nat × Nat) :

(start, stop).allI f a returns true if f is true for all natural numbers from start (inclusive) to stop (exclusive):

(5, 8).anyI f = f 5 && f 6 && f 7

Equations

Prod.allI f i = Nat.allTR.loop f i.snd (i.snd - i.fst)

Instances For