# 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 : NatSort u_1} (zero : motive 0) (succ : (n : Nat) → motive nmotive (n + 1)) :
Nat.recAux zero succ 0 = zero
theorem Nat.recAux_succ {motive : NatSort u_1} (zero : motive 0) (succ : (n : Nat) → motive nmotive (n + 1)) (n : Nat) :
Nat.recAux zero succ (n + 1) = succ n (Nat.recAux zero succ n)
@[simp]
theorem Nat.recAuxOn_zero {motive : NatSort u_1} (zero : motive 0) (succ : (n : Nat) → motive nmotive (n + 1)) :
Nat.recAuxOn 0 zero succ = zero
theorem Nat.recAuxOn_succ {motive : NatSort u_1} (zero : motive 0) (succ : (n : Nat) → motive nmotive (n + 1)) (n : Nat) :
Nat.recAuxOn (n + 1) zero succ = succ n (Nat.recAuxOn n zero succ)
@[simp]
theorem Nat.casesAuxOn_zero {motive : NatSort u_1} (zero : motive 0) (succ : (n : Nat) → motive (n + 1)) :
Nat.casesAuxOn 0 zero succ = zero
theorem Nat.casesAuxOn_succ {motive : NatSort 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 : NatSort u_1} (ind : (n : Nat) → ((m : Nat) → m < nmotive 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 : NatSort u_1} (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) (t : Nat) :
t.strongRecOn ind = ind t fun (m : Nat) (x : m < t) => m.strongRecOn ind
@[simp]
theorem Nat.recDiagAux_zero_left {motive : NatNatSort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m nmotive (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 : NatNatSort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m nmotive (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 : NatNatSort u_1} (zero_left : (n : Nat) → motive 0 n) (zero_right : (m : Nat) → motive m 0) (succ_succ : (m n : Nat) → motive m nmotive (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 : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (m + 1) (n + 1)) :
Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 0 = zero_zero
theorem Nat.recDiag_zero_succ {motive : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (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 : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (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 : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (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 : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (m + 1) (n + 1)) :
Nat.recDiagOn 0 0 zero_zero zero_succ succ_zero succ_succ = zero_zero
theorem Nat.recDiagOn_zero_succ {motive : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (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 : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (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 : NatNatSort u_1} (zero_zero : motive 0 0) (zero_succ : (n : Nat) → motive 0 nmotive 0 (n + 1)) (succ_zero : (m : Nat) → motive m 0motive (m + 1) 0) (succ_succ : (m n : Nat) → motive m nmotive (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 : NatNatSort 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 : NatNatSort 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 : NatNatSort 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 : NatNatSort 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

## strong case #

def Nat.lt_sum_ge (a : Nat) (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 else
Instances For
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
Instances For

a.succ + b = a + b.succ

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 mn - k m - kn 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 kk - m k - nn m

Alias of Nat.le_of_sub_le_sub_left.

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

### sum #

@[simp]
theorem Nat.sum_nil :
Nat.sum [] = 0
@[simp]
theorem Nat.sum_cons {a : Nat} {l : } :
Nat.sum (a :: l) = a +
@[simp]
theorem Nat.sum_append {l₁ : } {l₂ : } :
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.