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

source
@[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
source
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)
source
@[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
source
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)
source
@[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
source
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
source
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
source
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
source
@[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
source
@[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 : zero_left 0 = zero_right 0 := by first | assumption | trivial) :
Nat.recDiagAux zero_left zero_right succ_succ m 0 = zero_right m
source
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 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)
source
@[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
source
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)
source
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)
source
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 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)
source
@[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
source
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)
source
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)
source
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 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)
source
@[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
source
@[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
source
@[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
source
@[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 n : Nat) :
Nat.casesDiagOn (m + 1) (n + 1) zero_zero zero_succ succ_zero succ_succ = succ_succ m n

## strong case #

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

Strong case analysis on `a < b ∨ b ≤ a`

Equations

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

Instances For

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

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

Equations

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

Instances For

### div/mod #

### sum #

source
@[deprecated List.sum_append_nat (since := "2025-07-31")]
theorem Nat.sum_append {l₁ l₂ : List Nat} :
(l₁ ++ l₂).sum = l₁.sum + l₂.sum

Alias of `List.sum_append_nat`.

### ofBits #

source
@[simp]
theorem Nat.ofBits_zero (f : Fin 0 → Bool) :
ofBits f = 0
source
theorem Nat.ofBits_succ {n : Nat} (f : Fin (n + 1) → Bool) :
ofBits f = 2 * ofBits (f ∘ Fin.succ) + (f 0).toNat
source
theorem Nat.ofBits_lt_two_pow {n : Nat} (f : Fin n → Bool) :
ofBits f < 2 ^ n
source
@[simp]
theorem Nat.testBit_ofBits_lt {n : Nat} (f : Fin n → Bool) (i : Nat) (h : i < n) :
(ofBits f).testBit i = f ⟨i, h⟩
source
@[simp]
theorem Nat.testBit_ofBits_ge {n : Nat} (f : Fin n → Bool) (i : Nat) (h : n ≤ i) :
(ofBits f).testBit i = false
source
theorem Nat.testBit_ofBits {n i : Nat} (f : Fin n → Bool) :
(ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else false
source
theorem Nat.ofBits_testBit (x n : Nat) :
(ofBits fun (i : Fin n) => x.testBit ↑i) = x % 2 ^ n

### Misc #

source
theorem Nat.mul_add_lt_mul_of_lt_of_lt {m n x y : Nat} (hx : x < m) (hy : y < n) :
n * x + y < m * n
source
theorem Nat.add_mul_lt_mul_of_lt_of_lt {m n x y : Nat} (hx : x < m) (hy : y < n) :
x + m * y < m * n