# Documentation

## Init.Data.Nat.Basic

@[reducible, inline]
abbrev Nat.recAux {motive : NatSort u} (zero : motive 0) (succ : (n : Nat) → motive nmotive (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
Instances For
@[reducible, inline]
abbrev Nat.casesAuxOn {motive : NatSort 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
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
Instances For
@[inline]
def Nat.foldTR {α : Type u} (f : Natαα) (n : Nat) (init : α) :
α

Tail-recursive version of Nat.fold.

Equations
Instances For
@[specialize #[]]
def Nat.foldTR.loop {α : Type u} (f : Natαα) (n : Nat) :
Natαα
Equations
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
Instances For
@[specialize #[]]
def Nat.any (f : ) :

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

Equations
Instances For
@[inline]
def Nat.anyTR (f : ) (n : Nat) :

Tail-recursive version of Nat.any.

Equations
Instances For
@[specialize #[]]
def Nat.anyTR.loop (f : ) (n : Nat) :
Equations
Instances For
@[specialize #[]]
def Nat.all (f : ) :

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

Equations
Instances For
@[inline]
def Nat.allTR (f : ) (n : Nat) :

Tail-recursive version of Nat.all.

Equations
Instances For
@[specialize #[]]
def Nat.allTR.loop (f : ) (n : Nat) :
Equations
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
Instances For
@[inline]
def Nat.repeatTR {α : Type u} (f : αα) (n : Nat) (a : α) :
α

Tail-recursive version of Nat.repeat.

Equations
Instances For
@[specialize #[]]
def Nat.repeatTR.loop {α : Type u} (f : αα) :
Natαα
Equations
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

# 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)
Equations
@[simp]
theorem Nat.beq_eq_true_eq (a : Nat) (b : Nat) :
((a == b) = true) = (a = b)
@[simp]
theorem Nat.not_beq_eq_true_eq (a : Nat) (b : Nat) :
((!a == b) = true) = ¬a = b

@[simp]
theorem Nat.zero_add (n : Nat) :
0 + n = n
Std.LawfulIdentity (fun (x x_1 : Nat) => x + x_1) 0
Equations
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
@[simp]
theorem Nat.zero_ne_add_one (n : Nat) :
0 n + 1
theorem Nat.add_comm (n : Nat) (m : Nat) :
n + m = m + n
Std.Commutative fun (x x_1 : Nat) => x + x_1
Equations
theorem Nat.add_assoc (n : Nat) (m : Nat) (k : Nat) :
n + m + k = n + (m + k)
Std.Associative fun (x x_1 : Nat) => x + x_1
Equations
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 + km = 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 = 0n = 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
@[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.mul_comm (n : Nat) (m : Nat) :
n * m = m * n
instance Nat.instCommutativeHMul :
Std.Commutative fun (x x_1 : Nat) => x * x_1
Equations
@[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 (x x_1 : Nat) => x * x_1) 1
Equations
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 (x x_1 : Nat) => x * x_1
Equations
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 < mn.succ < m.succ
theorem Nat.lt_succ_of_le {n : Nat} {m : Nat} :
n mn < m.succ
@[simp]
theorem Nat.sub_zero (n : Nat) :
n - 0 = n
theorem Nat.succ_sub_succ_eq_sub (n : Nat) (m : Nat) :
n.succ - m.succ = n - m
@[simp]
theorem Nat.pred_le (n : Nat) :
n.pred n
theorem Nat.pred_lt {n : Nat} :
n 0n.pred < n
theorem Nat.sub_le (n : Nat) (m : Nat) :
n - m n
theorem Nat.sub_lt {n : Nat} {m : Nat} :
0 < n0 < mn - 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 < mm kn < k
theorem Nat.lt_of_lt_of_eq {n : Nat} {m : Nat} {k : Nat} :
n < mm = kn < k
instance Nat.instTransLt :
Trans (fun (x x_1 : Nat) => x < x_1) (fun (x x_1 : Nat) => x < x_1) fun (x x_1 : Nat) => x < x_1
Equations
instance Nat.instTransLe :
Trans (fun (x x_1 : Nat) => x x_1) (fun (x x_1 : Nat) => x x_1) fun (x x_1 : Nat) => x x_1
Equations
instance Nat.instTransLtLe :
Trans (fun (x x_1 : Nat) => x < x_1) (fun (x x_1 : Nat) => x x_1) fun (x x_1 : Nat) => x < x_1
Equations
instance Nat.instTransLeLt :
Trans (fun (x x_1 : Nat) => x x_1) (fun (x x_1 : Nat) => x < x_1) fun (x x_1 : Nat) => x < x_1
Equations
theorem Nat.le_of_eq {n : Nat} {m : Nat} (p : n = m) :
n m
theorem Nat.lt.step {n : Nat} {m : Nat} :
n < mn < 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 < mn < m
theorem Nat.le_of_lt {n : Nat} {m : Nat} :
n < mn m
theorem Nat.lt_of_succ_lt_succ {n : Nat} {m : Nat} :
n.succ < m.succn < 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 00 < n
theorem Nat.lt.base (n : Nat) :
n < n.succ
@[simp]
theorem Nat.lt_succ_self (n : Nat) :
n < n.succ
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 < b0 < 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_add_right (n : Nat) (k : Nat) :
n n + k
theorem Nat.le_add_left (n : Nat) (m : Nat) :
n m + n
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.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) :
¬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 ab < a
theorem Nat.lt_of_not_le {a : Nat} {b : Nat} :
¬a bb < 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 > ab a
theorem Nat.le_of_not_lt {a : Nat} {b : Nat} :
¬a < bb 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 < bb 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 ba 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 ba < 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 :
Antisymm fun (x x_1 : Nat) => x x_1
Equations
instance Nat.instAntisymmNotLt :
Antisymm fun (x x_1 : Nat) => ¬x < x_1
Equations
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_right {k : Nat} {n : Nat} (h : 0 < k) :
n < n + k
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 + ba c
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
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
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
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
Instances For
@[reducible, inline]
abbrev Nat.le_or_ge (m : Nat) (n : Nat) :
m n n m

Alias for Nat.le_total.

Equations
Instances For
@[reducible, inline]
abbrev Nat.le_or_le (m : Nat) (n : Nat) :
m n n m

Alias for Nat.le_total.

Equations
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_succ_iff_lt_or_eq {m : Nat} {n : Nat} :
m < n.succ 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
Instances For
theorem Nat.two_pos :
0 < 2
theorem Nat.ne_zero_iff_zero_lt {n : Nat} :
n 0 0 < n
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.succ_le {n : Nat} {m : Nat} :
n.succ 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.succ_pred_eq_of_ne_zero {n : Nat} :
n 0n.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.pred_inj {a : Nat} {b : Nat} :
0 < a0 < ba.pred = b.preda = b
theorem Nat.pred_ne_self {a : Nat} :
a 0a.pred a
theorem Nat.pred_lt_self {a : Nat} :
0 < aa.pred < a
theorem Nat.pred_lt_pred {n : Nat} {m : Nat} :
n 0n < mn.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 mn m.succ
theorem Nat.pred_le_of_le_succ {n : Nat} {m : Nat} :
n m.succn.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.predn.succ < m
theorem Nat.lt_pred_of_succ_lt {n : Nat} {m : Nat} :
n.succ < mn < 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 < ba b - 1
theorem Nat.lt_of_le_pred {m : Nat} {n : Nat} (h : 0 < m) :
n m.predn < m
theorem Nat.exists_eq_succ_of_ne_zero {n : Nat} :
n 0∃ (k : Nat), n = k.succ

# Basic theorems for comparing numerals #

@[simp]
theorem Nat.succ_ne_zero (n : Nat) :
n.succ 0

# 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
@[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 jn ^ i n ^ j
theorem Nat.pos_pow_of_pos {n : Nat} (m : Nat) (h : 0 < n) :
0 < n ^ m

# 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
Instances For
theorem Nat.min_def {n : Nat} {m : Nat} :
min n m = if n m then n else m
instance Nat.instMax :
Equations
@[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
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' {n : Nat} {m : Nat} (h : m < n) :
n.pred < n

# pred theorems #

@[simp]
theorem Nat.pred_zero :
= 0
@[simp]
theorem Nat.pred_succ (n : Nat) :
n.succ.pred = n
theorem Nat.succ_pred {a : Nat} (h : a 0) :
a.pred.succ = a
theorem Nat.succ_pred_eq_of_pos {n : Nat} :
0 < nn.pred.succ = n
theorem Nat.sub_one_add_one_eq_of_pos {n : Nat} :
0 < nn - 1 + 1 = n
@[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 < bb - a 0
theorem Nat.add_sub_of_le {a : Nat} {b : Nat} (h : a b) :
a + (b - 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 < mk < nm - n < m - k
@[simp]
theorem Nat.zero_sub (n : Nat) :
0 - n = 0
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 : } (x : Nat) (y : Nat) (h₁ : y x∀ (k : Nat), x = y + kmotive k) (h₂ : x < ymotive 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.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.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 = 0n m
theorem Nat.le_of_sub_le_sub_right {n : Nat} {m : Nat} {k : Nat} :
k mn - k m - kn 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.mul_pred_left (n : Nat) (m : Nat) :
n.pred * m = n * m - m

## Mul sub distrib #

theorem Nat.mul_pred_right (n : Nat) (m : Nat) :
n * m.pred = 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.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.go (f : ) (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.go (f : ) (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.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 : ) (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
Instances For
@[inline]
def Prod.anyI (f : ) (i : ) :

(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
Instances For
@[inline]
def Prod.allI (f : ) (i : ) :

(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
Instances For