Init.Data.Nat.Basic

source

@[specialize]

def Nat.foldAux {α : Type u} (f : Nat → α → α) (s : Nat) :

Nat → α → α

Equations

Nat.foldAux f s 0 _fun_discr = _fun_discr
Nat.foldAux f s (Nat.succ n) _fun_discr = Nat.foldAux f s n (f (s - Nat.succ n) _fun_discr)

source

@[inline]

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

α

Equations

Nat.fold f n init = Nat.foldAux f n n init

source

@[inline]

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

α

Equations

Nat.foldRev f n init = Nat.foldRev.loop f n init

source

@[specialize]

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

Nat → α → α

Equations

Nat.foldRev.loop f 0 _fun_discr = _fun_discr
Nat.foldRev.loop f (Nat.succ n) _fun_discr = Nat.foldRev.loop f n (f n _fun_discr)

source

@[specialize]

def Nat.anyAux (f : Nat → Bool) (s : Nat) :

Nat → Bool

Equations

Nat.anyAux f s 0 = false
Nat.anyAux f s (Nat.succ n) = (f (s - Nat.succ n) || Nat.anyAux f s n)

source

@[inline]

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

Bool

Equations

Nat.any f n = Nat.anyAux f n n

source

@[inline]

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

Bool

Equations

Nat.all f n = !Nat.any (fun i => !f i) n

source

@[inline]

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

α

Equations

Nat.repeat f n a = Nat.repeat.loop f n a

source

@[specialize]

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

Nat → α → α

Equations

Nat.repeat.loop f 0 _fun_discr = _fun_discr
Nat.repeat.loop f (Nat.succ n) _fun_discr = Nat.repeat.loop f n (f _fun_discr)

source

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

Bool

Equations

Nat.blt a b = Nat.ble (Nat.succ a) b

source

@[simp]

theorem Nat.zero_eq :

Nat.zero = 0

source

@[simp]

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

Nat.add x y = x + y

source

@[simp]

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

Nat.mul x y = x * y

source

@[simp]

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

Nat.sub x y = x - y

source

@[simp]

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

Nat.lt x y = (x < y)

source

@[simp]

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

Nat.le x y = (x ≤ y)

source

@[simp]

theorem Nat.beq_refl (a : Nat) :

Nat.beq a a = true

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

noncomputable instance Nat.instLawfulBEqNatInstBEqNat :

LawfulBEq Nat

Equations

Nat.instLawfulBEqNatInstBEqNat = Nat.instLawfulBEqNatInstBEqNat.proof_1

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

theorem Nat.zero_add (n : Nat) :

0 + n = n

source

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

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

source

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

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

source

theorem Nat.add_one (n : Nat) :

n + 1 = Nat.succ n

source

theorem Nat.succ_eq_add_one (n : Nat) :

Nat.succ n = n + 1

source

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

n + m = m + n

source

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

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

source

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

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

source

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

n + m + k = n + k + m

source

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

n + m = n + k → m = k

source

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

n = k

source

@[simp]

theorem Nat.mul_zero (n : Nat) :

n * 0 = 0

source

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

n * Nat.succ m = n * m + n

source

@[simp]

theorem Nat.zero_mul (n : Nat) :

0 * n = 0

source

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

Nat.succ n * m = n * m + m

source

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

n * m = m * n

source

@[simp]

theorem Nat.mul_one (n : Nat) :

n * 1 = n

source

@[simp]

theorem Nat.one_mul (n : Nat) :

1 * n = n

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

n < m → Nat.succ n < Nat.succ m

source

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

n ≤ m → n < Nat.succ m

source

@[simp]

theorem Nat.sub_zero (n : Nat) :

n - 0 = n

source

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

Nat.succ n - Nat.succ m = n - m

source

theorem Nat.pred_le (n : Nat) :

Nat.pred n ≤ n

source

theorem Nat.pred_lt {n : Nat} :

n ≠ 0 → Nat.pred n < n

source

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

n - m ≤ n

source

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

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

source

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

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

source

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

Nat.succ n - Nat.succ m = n - m

source

@[simp]

theorem Nat.sub_self (n : Nat) :

n - n = 0

source

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

n < m → m ≤ k → n < k

source

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

n < m → m = k → n < k

source

instance Nat.instTransNatLtInstLTNat :

Trans (fun a a_1 => a < a_1) (fun a a_1 => a < a_1) fun a a_1 => a < a_1

Equations

Nat.instTransNatLtInstLTNat = { trans := @Nat.instTransNatLtInstLTNat.proof_1 }

source

instance Nat.instTransNatLeInstLENat :

Trans (fun a a_1 => a ≤ a_1) (fun a a_1 => a ≤ a_1) fun a a_1 => a ≤ a_1

Equations

Nat.instTransNatLeInstLENat = { trans := @Nat.instTransNatLeInstLENat.proof_1 }

source

instance Nat.instTransNatLtInstLTNatLeInstLENat :

Trans (fun a a_1 => a < a_1) (fun a a_1 => a ≤ a_1) fun a a_1 => a < a_1

Equations

Nat.instTransNatLtInstLTNatLeInstLENat = { trans := @Nat.instTransNatLtInstLTNatLeInstLENat.proof_1 }

source

instance Nat.instTransNatLeInstLENatLtInstLTNat :

Trans (fun a a_1 => a ≤ a_1) (fun a a_1 => a < a_1) fun a a_1 => a < a_1

Equations

Nat.instTransNatLeInstLENatLtInstLTNat = { trans := @Nat.instTransNatLeInstLENatLtInstLTNat.proof_1 }

source

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

n ≤ m

source

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

n ≤ m

source

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

n ≤ m

source

noncomputable def Nat.lt.step {n : Nat} {m : Nat} :

n < m → n < Nat.succ m

Equations

@Nat.lt.step = @Nat.lt.step.proof_1

source

theorem Nat.eq_zero_or_pos (n : Nat) :

n = 0 ∨ n > 0

source

noncomputable def Nat.lt.base (n : Nat) :

n < Nat.succ n

Equations

Nat.lt.base = Nat.lt.base.proof_1

source

theorem Nat.lt_succ_self (n : Nat) :

n < Nat.succ n

source

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

m ≤ n ∨ n ≤ m

source

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

n = 0

source

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

Nat.succ n < m → n < m

source

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

Nat.succ n < Nat.succ m → n < m

source

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

n < m

source

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

Nat.succ n ≤ m

source

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

a ≠ b

source

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

m ≤ n ∨ m = Nat.succ n

source

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

n ≤ n + k

source

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

n ≤ m + n

source

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

n ≤ m → ∃ k, n + k = m

source

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

n ≤ m

source

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

¬n ≤ m

source

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

n > m

source

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

n ≥ m

source

instance Nat.instAntisymmNatLeInstLENat :

Antisymm fun a a_1 => a ≤ a_1

Equations

Nat.instAntisymmNatLeInstLENat = { antisymm := @Nat.instAntisymmNatLeInstLENat.proof_1 }

source

instance Nat.instAntisymmNatNotLtInstLTNat :

Antisymm fun a a_1 => ¬a < a_1

Equations

Nat.instAntisymmNatNotLtInstLTNat = { antisymm := @Nat.instAntisymmNatNotLtInstLTNat.proof_1 }

source

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

k + n ≤ k + m

source

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

n + k ≤ m + k

source

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

k + n < k + m

source

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

n + k < m + k

source

theorem Nat.zero_lt_one :

0 < 1

source

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

a + c ≤ b + d

source

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

a + c < b + d

source

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

b ≤ c

source

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

∀ (a : a + b ≤ c + b), a ≤ c

source

theorem Nat.ctor_eq_zero :

Nat.zero = 0

source

theorem Nat.one_ne_zero :

1 ≠ 0

source

theorem Nat.zero_ne_one :

0 ≠ 1

source

theorem Nat.succ_ne_zero (n : Nat) :

Nat.succ n ≠ 0

source

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

k * n ≤ k * m

source

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

n * k ≤ m * k

source

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

n₁ * m₁ ≤ n₂ * m₂

source

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

k * n < k * m

source

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

n * k < m * k

source

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

n * m > 0

source

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

a ≤ b

source

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

m = k

source

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

n = k

source

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

n ^ Nat.succ m = n ^ m * n

source

theorem Nat.pow_zero (n : Nat) :

n ^ 0 = 1

source

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

n ^ i ≤ m ^ i

source

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

i ≤ j → n ^ i ≤ n ^ j

source

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

0 < n ^ m

source

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

Nat

Equations

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

source

def Nat.max (n : Nat) (m : Nat) :

Nat

Equations

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

source

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

a ≠ 0

source

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

Nat.pred n < n

source

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

a + b - a = b

source

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

a + b - b = a

source

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

a - i ≤ Nat.succ a - i

source

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

0 < a - i

source

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

a - (i + 1) < a - i

source

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

Nat.succ (Nat.pred a) = a

source

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

∀ (a : a < b), b - a ≠ 0

source

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

a + (b - a) = b

source

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

n - m + m = n

source

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

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

source

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

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

source

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

n + m - m = n

source

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

n + m - n = m

source

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

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

source

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

a = c + b

source

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

a - b = c

source

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

a ≤ c + b

source

@[simp]

theorem Nat.zero_sub (n : Nat) :

0 - n = 0

source

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

n - (n + m) = 0

source

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

n - m = 0

source

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

a - b ≤ c

source

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

a + b ≤ c

source

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

a ≤ c - b

source

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

a + b < c

source

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

a < c - b

source

@[simp]

theorem Nat.pred_zero :

Nat.pred 0 = 0

source

@[simp]

theorem Nat.pred_succ (n : Nat) :

Nat.pred (Nat.succ n) = n

source

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)

source

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

Nat.pred n * m = n * m - m

source

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

n * Nat.pred m = n * m - n

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

source

@[inline]

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

α

Equations

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

source

@[inline]

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

Bool

Equations

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

source

@[inline]

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

Bool

Equations

Prod.allI f i = Nat.anyAux (fun a => !f a) i.snd (i.snd - i.fst)