Basic lemmas about natural numbers

The primary purpose of the lemmas in this file is to assist with reasoning about sizes of objects, array indices and such. For a more thorough development of the theory of natural numbers, we recommend using Mathlib.

rec/cases

@[simp]

theorem Nat.recAux_zero {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) : Nat.recAux zero succ 0 = zero

theorem Nat.recAux_succ {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (n : Nat) : Nat.recAux zero succ (n + 1) = succ n (Nat.recAux zero succ n)

@[simp]

theorem Nat.recAuxOn_zero {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) : Nat.recAuxOn 0 zero succ = zero

theorem Nat.recAuxOn_succ {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive n → motive (n + 1)) (n : Nat) : Nat.recAuxOn (n + 1) zero succ = succ n (Nat.recAuxOn n zero succ)

@[simp]

theorem Nat.casesAuxOn_zero {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) : Nat.casesAuxOn 0 zero succ = zero

@[simp]

theorem Nat.casesAuxOn_succ {motive : Nat → Sort u_1} (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) (n : Nat) : Nat.casesAuxOn (n + 1) zero succ = succ n

theorem Nat.strongRec_eq {motive : Nat → Sort u_1} (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) (t : Nat) : Nat.strongRec ind t = ind t fun (m : Nat) (x : m < t) => Nat.strongRec ind m

theorem Nat.strongRecOn_eq {motive : Nat → Sort u_1} (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) (t : Nat) : Nat.strongRecOn t ind = ind t fun (m : Nat) (x : m < t) => Nat.strongRecOn m ind

@[simp]

theorem Nat.recDiagAux_zero_left {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (n : Nat) : Nat.recDiagAux zero_left zero_right succ_succ 0 n = zero_left n

@[simp]

theorem Nat.recDiagAux_zero_right {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (h : autoParam (zero_left 0 = zero_right 0) _auto✝) : Nat.recDiagAux zero_left zero_right succ_succ m 0 = zero_right m

theorem Nat.recDiagAux_succ_succ {motive : Nat → Nat → Sort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : Nat.recDiagAux zero_left zero_right succ_succ (m + 1) (n + 1) = succ_succ m n (Nat.recDiagAux zero_left zero_right succ_succ m n)

@[simp]

theorem Nat.recDiag_zero_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 0 = zero_zero

theorem Nat.recDiag_zero_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (n : Nat) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 (n + 1) = zero_succ n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 n)

theorem Nat.recDiag_succ_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) 0 = succ_zero m (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m 0)

theorem Nat.recDiag_succ_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : Nat.recDiag zero_zero zero_succ succ_zero succ_succ (m + 1) (n + 1) = succ_succ m n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ m n)

@[simp]

theorem Nat.recDiagOn_zero_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) : Nat.recDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero

theorem Nat.recDiagOn_zero_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (n : Nat) : Nat.recDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ = zero_succ n (Nat.recDiagOn 0 n zero_zero zero_succ succ_zero succ_succ)

theorem Nat.recDiagOn_succ_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) : Nat.recDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m (Nat.recDiagOn m 0 zero_zero zero_succ succ_zero succ_succ)

theorem Nat.recDiagOn_succ_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 n → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m n → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : Nat.recDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n (Nat.recDiagOn m n zero_zero zero_succ succ_zero succ_succ)

@[simp]

theorem Nat.casesDiagOn_zero_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) : Nat.casesDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero

@[simp]

theorem Nat.casesDiagOn_zero_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) (n : Nat) : Nat.casesDiagOn 0 (n + 1) zero_zero zero_succ succ_zero succ_succ = zero_succ n

@[simp]

theorem Nat.casesDiagOn_succ_zero {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) (m : Nat) : Nat.casesDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m

@[simp]

theorem Nat.casesDiagOn_succ_succ {motive : Nat → Nat → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 (n + 1)) (succ_zero : (m : Nat) → motive (m + 1) 0) (succ_succ : (m n : Nat) → motive (m + 1) (n + 1)) (m : Nat) (n : Nat) : Nat.casesDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n

compare

theorem Nat.compare_def_lt (a : Nat) (b : Nat) : compare a b = if a < b then Ordering.lt else if b < a then Ordering.gt else Ordering.eq

theorem Nat.compare_def_le (a : Nat) (b : Nat) : compare a b = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt

theorem Nat.compare_swap (a : Nat) (b : Nat) : Ordering.swap (compare a b) = compare b a

theorem Nat.compare_eq_eq {a : Nat} {b : Nat} : compare a b = Ordering.eq ↔ a = b

theorem Nat.compare_eq_lt {a : Nat} {b : Nat} : compare a b = Ordering.lt ↔ a < b

theorem Nat.compare_eq_gt {a : Nat} {b : Nat} : compare a b = Ordering.gt ↔ b < a

theorem Nat.compare_ne_gt {a : Nat} {b : Nat} : compare a b ≠ Ordering.gt ↔ a ≤ b

theorem Nat.compare_ne_lt {a : Nat} {b : Nat} : compare a b ≠ Ordering.lt ↔ b ≤ a

def Nat.lt_sum_ge (a : Nat) (b : Nat) : a < b ⊕' b ≤ a

Strong case analysis on a < b ∨ b ≤ a

Equations

• Nat.lt_sum_ge a b = if h : a < b then PSum.inl h else PSum.inr ⋯

def Nat.sum_trichotomy (a : Nat) (b : Nat) : a < b ⊕' a = b ⊕' b < a

Strong case analysis on a < b ∨ a = b ∨ b < a

Equations

• Nat.sum_trichotomy a b = match h : compare a b with | Ordering.lt => PSum.inl ⋯ | Ordering.eq => PSum.inr (PSum.inl ⋯) | Ordering.gt => PSum.inr (PSum.inr ⋯)

add

@[deprecated Nat.succ_add_eq_add_succ]

theorem Nat.succ_add_eq_succ_add (a : Nat) (b : Nat) : Nat.succ a + b = a + Nat.succ b

Alias of Nat.succ_add_eq_add_succ.

sub

@[deprecated Nat.le_of_sub_le_sub_right]

theorem Nat.le_of_le_of_sub_le_sub_right {n : Nat} {m : Nat} {k : Nat} : k ≤ m → n - k ≤ m - k → n ≤ m

Alias of Nat.le_of_sub_le_sub_right.

@[deprecated Nat.le_of_sub_le_sub_left]

theorem Nat.le_of_le_of_sub_le_sub_left {n : Nat} {k : Nat} {m : Nat} : n ≤ k → k - m ≤ k - n → n ≤ m

Alias of Nat.le_of_sub_le_sub_left.

min/max

theorem Nat.sub_min_sub_left (a : Nat) (b : Nat) (c : Nat) : min (a - b) (a - c) = a - max b c

theorem Nat.sub_max_sub_left (a : Nat) (b : Nat) (c : Nat) : max (a - b) (a - c) = a - min b c

theorem Nat.mul_max_mul_right (a : Nat) (b : Nat) (c : Nat) : max (a * c) (b * c) = max a b * c

theorem Nat.mul_min_mul_right (a : Nat) (b : Nat) (c : Nat) : min (a * c) (b * c) = min a b * c

theorem Nat.mul_max_mul_left (a : Nat) (b : Nat) (c : Nat) : max (a * b) (a * c) = a * max b c

theorem Nat.mul_min_mul_left (a : Nat) (b : Nat) (c : Nat) : min (a * b) (a * c) = a * min b c

mul

@[deprecated Nat.mul_lt_mul_of_lt_of_le']

theorem Nat.mul_lt_mul {a : Nat} {c : Nat} {b : Nat} {d : Nat} (hac : a < c) (hbd : b ≤ d) (hb : 0 < b) : a * b < c * d

Alias of Nat.mul_lt_mul_of_lt_of_le'.

@[deprecated Nat.mul_lt_mul_of_le_of_lt]

theorem Nat.mul_lt_mul' {a : Nat} {c : Nat} {b : Nat} {d : Nat} (hac : a ≤ c) (hbd : b < d) (hc : 0 < c) : a * b < c * d

Alias of Nat.mul_lt_mul_of_le_of_lt.

div/mod

sum

@[simp]

theorem Nat.sum_nil : Nat.sum [] = 0

@[simp]

theorem Nat.sum_cons {a : Nat} {l : List Nat} : Nat.sum (a :: l) = a + Nat.sum l

@[simp]

theorem Nat.sum_append {l₁ : List Nat} {l₂ : List Nat} : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂

@[deprecated Nat.lt_or_gt_of_ne]

theorem Nat.lt_connex {a : Nat} {b : Nat} (ne : a ≠ b) : a < b ∨ a > b

Alias of Nat.lt_or_gt_of_ne.

@[deprecated Nat.two_pow_pos]

theorem Nat.pow_two_pos (w : Nat) : 0 < 2 ^ w

Alias of Nat.two_pow_pos.