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

le/lt

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

theorem Nat.ne_of_lt' {a : Nat} {b : Nat} (h : b < a) : a ≠ b

Alias of Nat.ne_of_gt.

theorem Nat.lt_of_not_ge {a : Nat} {b : Nat} : ¬a ≤ b → b < a

Alias of the forward direction of Nat.not_le.

theorem Nat.not_le_of_lt {a : Nat} {b : Nat} : b < a → ¬a ≤ b

Alias of the reverse direction of Nat.not_le.

theorem Nat.lt_of_not_le {a : Nat} {b : Nat} : ¬a ≤ b → b < a

Alias of the forward direction of Nat.not_le.

theorem Nat.lt_le_asymm {a : Nat} {b : Nat} : b < a → ¬a ≤ b

Alias of the reverse direction of Nat.not_le.

theorem Nat.le_of_not_gt {a : Nat} {b : Nat} : ¬a < b → b ≤ a

Alias of the forward direction of Nat.not_lt.

theorem Nat.not_lt_of_ge {a : Nat} {b : Nat} : b ≤ a → ¬a < b

Alias of the reverse direction of Nat.not_lt.

theorem Nat.le_of_not_lt {a : Nat} {b : Nat} : ¬a < b → b ≤ a

Alias of the forward direction of Nat.not_lt.

theorem Nat.not_lt_of_le {a : Nat} {b : Nat} : b ≤ a → ¬a < b

Alias of the reverse direction of Nat.not_lt.

theorem Nat.le_lt_asymm {a : Nat} {b : Nat} : b ≤ a → ¬a < b

Alias of the reverse direction of Nat.not_lt.

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} (h : ¬b ≤ a) : a ≤ b

Alias of Nat.le_of_not_le.

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

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

Alias of Nat.lt_asymm.

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

Alias of Nat.lt_asymm.

theorem Nat.lt_iff_le_not_le {m : Nat} {n : Nat} : m < n ↔ m ≤ n ∧ ¬n ≤ m

theorem Nat.lt_iff_le_and_not_ge {m : Nat} {n : Nat} : m < n ↔ m ≤ n ∧ ¬n ≤ m

Alias of Nat.lt_iff_le_not_le.

theorem Nat.lt_iff_le_and_ne {m : Nat} {n : Nat} : m < n ↔ m ≤ n ∧ m ≠ n

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

Alias of Nat.le_antisymm_iff.

theorem Nat.lt_or_gt_of_ne {a : Nat} {b : Nat} : a ≠ b → a < b ∨ b < a

theorem Nat.lt_or_lt_of_ne {a : Nat} {b : Nat} : a ≠ b → a < b ∨ b < a

Alias of Nat.lt_or_gt_of_ne.

@[deprecated Nat.lt_or_gt_of_ne]

theorem Nat.lt_connex {a : Nat} {b : Nat} : a ≠ b → a < b ∨ b < a

Alias of Nat.lt_or_gt_of_ne.

theorem Nat.ne_iff_lt_or_gt {a : Nat} {b : Nat} : a ≠ b ↔ a < b ∨ b < a

theorem Nat.lt_or_gt {a : Nat} {b : Nat} : a ≠ b ↔ a < b ∨ b < a

Alias of Nat.ne_iff_lt_or_gt.

theorem Nat.le_or_ge (m : Nat) (n : Nat) : m ≤ n ∨ n ≤ m

Alias of Nat.le_total.

theorem Nat.le_or_le (m : Nat) (n : Nat) : m ≤ n ∨ n ≤ m

Alias of Nat.le_total.

theorem Nat.lt_trichotomy (a : Nat) (b : Nat) : a < b ∨ a = b ∨ b < a

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 < Nat.succ n ↔ m ≤ n

theorem Nat.lt_succ_iff_lt_or_eq {m : Nat} {n : Nat} : m < Nat.succ n ↔ m < n ∨ 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 (_ : b ≤ a)

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

• One or more equations did not get rendered due to their size.

zero/one/two

theorem Nat.pos_iff_ne_zero {n : Nat} : 0 < n ↔ n ≠ 0

theorem Nat.le_zero {i : Nat} : i ≤ 0 ↔ i = 0

theorem Nat.one_pos : 0 < 1

Alias of Nat.zero_lt_one.

theorem Nat.two_pos : 0 < 2

theorem Nat.add_one_ne_zero (n : Nat) : n + 1 ≠ 0

theorem Nat.ne_zero_iff_zero_lt {n : Nat} : n ≠ 0 ↔ 0 < n

theorem Nat.zero_lt_two : 0 < 2

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) : Nat.succ n ≠ n

theorem Nat.succ_le {n : Nat} {m : Nat} : Nat.succ n ≤ m ↔ n < m

theorem Nat.lt_succ {m : Nat} {n : Nat} : m < Nat.succ n ↔ m ≤ n

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

theorem Nat.succ_pred_eq_of_pos {n : Nat} : 0 < n → Nat.succ (Nat.pred n) = n

theorem Nat.succ_pred_eq_of_ne_zero {n : Nat} : n ≠ 0 → Nat.succ (Nat.pred n) = n

theorem Nat.eq_zero_or_eq_succ_pred (n : Nat) : n = 0 ∨ n = Nat.succ (Nat.pred n)

theorem Nat.exists_eq_succ_of_ne_zero {n : Nat} : n ≠ 0 → ∃ (k : Nat), n = Nat.succ k

theorem Nat.succ_inj' {a : Nat} {b : Nat} : Nat.succ a = Nat.succ b ↔ a = b

theorem Nat.succ_le_succ_iff {a : Nat} {b : Nat} : Nat.succ a ≤ Nat.succ b ↔ a ≤ b

theorem Nat.succ_lt_succ_iff {a : Nat} {b : Nat} : Nat.succ a < Nat.succ b ↔ a < b

theorem Nat.pred_inj {a : Nat} {b : Nat} : 0 < a → 0 < b → Nat.pred a = Nat.pred b → a = b

theorem Nat.pred_ne_self {a : Nat} : a ≠ 0 → Nat.pred a ≠ a

theorem Nat.pred_lt_self {a : Nat} : 0 < a → Nat.pred a < a

theorem Nat.pred_lt_pred {n : Nat} {m : Nat} : n ≠ 0 → n < m → Nat.pred n < Nat.pred m

theorem Nat.pred_le_iff_le_succ {n : Nat} {m : Nat} : Nat.pred n ≤ m ↔ n ≤ Nat.succ m

theorem Nat.le_succ_of_pred_le {n : Nat} {m : Nat} : Nat.pred n ≤ m → n ≤ Nat.succ m

theorem Nat.pred_le_of_le_succ {n : Nat} {m : Nat} : n ≤ Nat.succ m → Nat.pred n ≤ m

theorem Nat.lt_pred_iff_succ_lt {n : Nat} {m : Nat} : n < Nat.pred m ↔ Nat.succ n < m

theorem Nat.succ_lt_of_lt_pred {n : Nat} {m : Nat} : n < Nat.pred m → Nat.succ n < m

theorem Nat.lt_pred_of_succ_lt {n : Nat} {m : Nat} : Nat.succ n < m → n < Nat.pred m

theorem Nat.le_pred_iff_lt {n : Nat} {m : Nat} : 0 < m → (n ≤ Nat.pred m ↔ n < m)

theorem Nat.lt_of_le_pred {m : Nat} {n : Nat} (h : 0 < m) : n ≤ Nat.pred m → n < m

theorem Nat.le_pred_of_lt {n : Nat} {m : Nat} (h : n < m) : n ≤ Nat.pred m

add

theorem Nat.add_add_add_comm (a : Nat) (b : Nat) (c : Nat) (d : Nat) : a + b + (c + d) = a + c + (b + d)

theorem Nat.one_add (n : Nat) : 1 + n = Nat.succ n

theorem Nat.succ_eq_one_add (n : Nat) : Nat.succ n = 1 + n

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

@[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.

theorem Nat.eq_zero_of_add_eq_zero {n : Nat} {m : Nat} : n + m = 0 → n = 0 ∧ m = 0

theorem Nat.eq_zero_of_add_eq_zero_right {n : Nat} {m : Nat} (h : n + m = 0) : n = 0

theorem Nat.eq_zero_of_add_eq_zero_left {n : Nat} {m : Nat} (h : n + m = 0) : m = 0

theorem Nat.add_eq_zero_iff {n : Nat} {m : Nat} : n + m = 0 ↔ n = 0 ∧ m = 0

theorem Nat.add_left_cancel_iff {m : Nat} {k : Nat} {n : Nat} : n + m = n + k ↔ m = k

theorem Nat.add_right_cancel_iff {m : Nat} {k : Nat} {n : Nat} : m + n = k + n ↔ m = k

theorem Nat.add_le_add_iff_left {m : Nat} {k : Nat} {n : Nat} : n + m ≤ n + k ↔ m ≤ k

theorem Nat.add_le_add_iff_right {m : Nat} {k : Nat} {n : Nat} : m + n ≤ k + n ↔ m ≤ k

theorem Nat.lt_of_add_lt_add_right {k : Nat} {m : Nat} {n : Nat} : k + n < m + n → k < m

theorem Nat.lt_of_add_lt_add_left {k : Nat} {m : Nat} {n : Nat} : n + k < n + m → k < m

theorem Nat.add_lt_add_iff_left {k : Nat} {n : Nat} {m : Nat} : k + n < k + m ↔ n < m

theorem Nat.add_lt_add_iff_right {k : Nat} {n : Nat} {m : Nat} : n + k < m + k ↔ n < m

theorem Nat.add_lt_add_of_le_of_lt {a : Nat} {b : Nat} {c : Nat} {d : Nat} (hle : a ≤ b) (hlt : c < d) : a + c < b + d

theorem Nat.add_lt_add_of_lt_of_le {a : Nat} {b : Nat} {c : Nat} {d : Nat} (hlt : a < b) (hle : c ≤ d) : a + c < b + d

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.lt_add_of_pos_right {k : Nat} {n : Nat} (h : 0 < k) : n < n + k

theorem Nat.lt_add_of_pos_left {k : Nat} {n : Nat} : 0 < k → n < k + n

theorem Nat.pos_of_lt_add_right {n : Nat} {k : Nat} (h : n < n + k) : 0 < k

theorem Nat.pos_of_lt_add_left {n : Nat} {k : Nat} : n < k + n → 0 < k

theorem Nat.lt_add_right_iff_pos {n : Nat} {k : Nat} : n < n + k ↔ 0 < k

theorem Nat.lt_add_left_iff_pos {n : Nat} {k : Nat} : n < k + n ↔ 0 < k

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

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

theorem Nat.add_self_ne_one (n : Nat) : n + n ≠ 1

sub

theorem Nat.sub_one (n : Nat) : n - 1 = Nat.pred n

theorem Nat.one_sub (n : Nat) : 1 - n = if n = 0 then 1 else 0

theorem Nat.succ_sub_sub_succ (n : Nat) (m : Nat) (k : Nat) : Nat.succ n - m - Nat.succ k = n - m - k

theorem Nat.sub_right_comm (m : Nat) (n : Nat) (k : Nat) : m - n - k = m - k - n

theorem Nat.add_sub_cancel_right (n : Nat) (m : Nat) : n + m - m = n

theorem Nat.add_sub_cancel' {n : Nat} {m : Nat} (h : m ≤ n) : m + (n - m) = n

theorem Nat.succ_sub_one (n : Nat) : Nat.succ n - 1 = n

theorem Nat.add_one_sub_one (n : Nat) : n + 1 - 1 = n

theorem Nat.one_add_sub_one (n : Nat) : 1 + n - 1 = n

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.sub_sub_self {n : Nat} {m : Nat} (h : m ≤ n) : n - (n - m) = m

theorem Nat.sub_add_comm {n : Nat} {m : Nat} {k : Nat} (h : k ≤ n) : n + m - k = n - k + m

theorem Nat.le_of_sub_eq_zero {n : Nat} {m : Nat} : n - m = 0 → n ≤ m

theorem Nat.sub_eq_zero_iff_le {n : Nat} {m : Nat} : n - m = 0 ↔ n ≤ m

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.sub_pos_of_lt {m : Nat} {n : Nat} (h : m < n) : 0 < n - m

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

theorem Nat.sub_pos_iff_lt {n : Nat} {m : Nat} : 0 < n - m ↔ m < n

theorem Nat.lt_of_sub_eq_succ {m : Nat} {n : Nat} {l : Nat} (h : m - n = Nat.succ l) : n < m

theorem Nat.sub_le_iff_le_add {a : Nat} {b : Nat} {c : Nat} : a - b ≤ c ↔ a ≤ c + b

theorem Nat.sub_le_iff_le_add' {a : Nat} {b : Nat} {c : Nat} : a - b ≤ c ↔ a ≤ b + c

theorem Nat.le_sub_iff_add_le {k : Nat} {m : Nat} {n : Nat} (h : k ≤ m) : n ≤ m - k ↔ n + k ≤ m

@[deprecated Nat.le_sub_iff_add_le]

theorem Nat.add_le_to_le_sub {m : Nat} {k : Nat} (n : Nat) (h : m ≤ k) : n + m ≤ k ↔ n ≤ k - m

theorem Nat.add_le_of_le_sub' {n : Nat} {k : Nat} {m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k

@[deprecated Nat.add_le_of_le_sub']

theorem Nat.add_le_of_le_sub_left {n : Nat} {k : Nat} {m : Nat} (h : m ≤ k) : n ≤ k - m → m + n ≤ k

theorem Nat.le_sub_of_add_le' {n : Nat} {k : Nat} {m : Nat} : m + n ≤ k → n ≤ k - m

theorem Nat.le_sub_iff_add_le' {k : Nat} {m : Nat} {n : Nat} (h : k ≤ m) : n ≤ m - k ↔ k + n ≤ m

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

@[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.

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_le_sub_left {n : Nat} {m : Nat} (h : n ≤ m) (k : Nat) : k - m ≤ k - n

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

@[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.

theorem Nat.sub_le_sub_iff_left {n : Nat} {m : Nat} {k : Nat} (h : n ≤ k) : k - m ≤ k - n ↔ n ≤ m

theorem Nat.sub_lt_of_pos_le {a : Nat} {b : Nat} (h₀ : 0 < a) (h₁ : a ≤ b) : b - a < b

theorem Nat.sub_lt_self {a : Nat} {b : Nat} (h₀ : 0 < a) (h₁ : a ≤ b) : b - a < b

Alias of Nat.sub_lt_of_pos_le.

theorem Nat.add_lt_of_lt_sub' {a : Nat} {b : Nat} {c : Nat} : b < c - a → a + b < c

theorem Nat.sub_add_lt_sub {m : Nat} {k : Nat} {n : Nat} (h₁ : m + k ≤ n) (h₂ : 0 < k) : n - (m + k) < n - m

theorem Nat.le_sub_one_of_lt {a : Nat} {b : Nat} : a < b → a ≤ b - 1

theorem Nat.sub_one_lt_of_le {a : Nat} {b : Nat} (h₀ : 0 < a) (h₁ : a ≤ b) : a - 1 < b

theorem Nat.sub_lt_succ (a : Nat) (b : Nat) : a - b < Nat.succ a

theorem Nat.sub_one_sub_lt {i : Nat} {n : Nat} (h : i < n) : n - 1 - i < n

min/max

theorem Nat.succ_min_succ (x : Nat) (y : Nat) : min (Nat.succ x) (Nat.succ y) = Nat.succ (min x y)

@[simp]

theorem Nat.min_self (a : Nat) : min a a = a

@[simp]

theorem Nat.zero_min (a : Nat) : min 0 a = 0

@[simp]

theorem Nat.min_zero (a : Nat) : min a 0 = 0

theorem Nat.min_assoc (a : Nat) (b : Nat) (c : Nat) : min (min a b) c = min a (min b c)

theorem Nat.sub_sub_eq_min (a : Nat) (b : Nat) : a - (a - b) = min a b

theorem Nat.sub_eq_sub_min (n : Nat) (m : Nat) : n - m = n - min n m

@[simp]

theorem Nat.sub_add_min_cancel (n : Nat) (m : Nat) : n - m + min n m = n

theorem Nat.max_eq_right {a : Nat} {b : Nat} (h : a ≤ b) : max a b = b

theorem Nat.max_eq_left {a : Nat} {b : Nat} (h : b ≤ a) : max a b = a

theorem Nat.succ_max_succ (x : Nat) (y : Nat) : max (Nat.succ x) (Nat.succ y) = Nat.succ (max x y)

theorem Nat.max_le_of_le_of_le {a : Nat} {b : Nat} {c : Nat} : a ≤ c → b ≤ c → max a b ≤ c

theorem Nat.max_le {a : Nat} {b : Nat} {c : Nat} : max a b ≤ c ↔ a ≤ c ∧ b ≤ c

theorem Nat.max_lt {a : Nat} {b : Nat} {c : Nat} : max a b < c ↔ a < c ∧ b < c

@[simp]

theorem Nat.max_self (a : Nat) : max a a = a

@[simp]

theorem Nat.zero_max (a : Nat) : max 0 a = a

@[simp]

theorem Nat.max_zero (a : Nat) : max a 0 = a

theorem Nat.max_assoc (a : Nat) (b : Nat) (c : Nat) : max (max a b) c = max a (max b c)

theorem Nat.sub_add_eq_max (a : Nat) (b : Nat) : a - b + b = max a b

theorem Nat.sub_eq_max_sub (n : Nat) (m : Nat) : n - m = max n m - m

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

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

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

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

theorem Nat.add_max_add_right (a : Nat) (b : Nat) (c : Nat) : max (a + c) (b + c) = max a b + c

theorem Nat.add_min_add_right (a : Nat) (b : Nat) (c : Nat) : min (a + c) (b + c) = min a b + c

theorem Nat.add_max_add_left (a : Nat) (b : Nat) (c : Nat) : max (a + b) (a + c) = a + max b c

theorem Nat.add_min_add_left (a : Nat) (b : Nat) (c : Nat) : min (a + b) (a + c) = a + min b c

theorem Nat.pred_min_pred (x : Nat) (y : Nat) : min (Nat.pred x) (Nat.pred y) = Nat.pred (min x y)

theorem Nat.pred_max_pred (x : Nat) (y : Nat) : max (Nat.pred x) (Nat.pred y) = Nat.pred (max x y)

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

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

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_le_mul_left]

theorem Nat.mul_le_mul_of_nonneg_left {a : Nat} {b : Nat} {c : Nat} : a ≤ b → c * a ≤ c * b

@[deprecated Nat.mul_le_mul_right]

theorem Nat.mul_le_mul_of_nonneg_right {a : Nat} {b : Nat} {c : Nat} : a ≤ b → a * c ≤ b * c

theorem Nat.mul_right_comm (n : Nat) (m : Nat) (k : Nat) : n * m * k = n * k * m

theorem Nat.mul_mul_mul_comm (a : Nat) (b : Nat) (c : Nat) (d : Nat) : a * b * (c * d) = a * c * (b * d)

theorem Nat.mul_two (n : Nat) : n * 2 = n + n

theorem Nat.two_mul (n : Nat) : 2 * n = n + n

theorem Nat.mul_eq_zero {m : Nat} {n : Nat} : n * m = 0 ↔ n = 0 ∨ m = 0

theorem Nat.mul_ne_zero_iff {n : Nat} {m : Nat} : n * m ≠ 0 ↔ n ≠ 0 ∧ m ≠ 0

theorem Nat.mul_ne_zero {n : Nat} {m : Nat} : n ≠ 0 → m ≠ 0 → n * m ≠ 0

theorem Nat.ne_zero_of_mul_ne_zero_left {n : Nat} {m : Nat} (h : n * m ≠ 0) : n ≠ 0

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

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

theorem Nat.mul_left_cancel_iff {n : Nat} (p : 0 < n) (m : Nat) (k : Nat) : n * m = n * k ↔ m = k

theorem Nat.mul_right_cancel_iff {m : Nat} (p : 0 < m) (n : Nat) (k : Nat) : n * m = k * m ↔ n = k

theorem Nat.ne_zero_of_mul_ne_zero_right {n : Nat} {m : Nat} (h : n * m ≠ 0) : m ≠ 0

theorem Nat.le_mul_of_pos_left {n : Nat} (m : Nat) (h : 0 < n) : m ≤ n * m

theorem Nat.le_mul_of_pos_right {m : Nat} (n : Nat) (h : 0 < m) : n ≤ n * m

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

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

@[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'.

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

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

@[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.

theorem Nat.mul_lt_mul_of_lt_of_lt {a : Nat} {b : Nat} {c : Nat} {d : Nat} (hac : a < c) (hbd : b < d) : a * b < c * d

theorem Nat.succ_mul_succ (a : Nat) (b : Nat) : Nat.succ a * Nat.succ b = a * b + a + b + 1

theorem Nat.mul_le_add_right (m : Nat) (k : Nat) (n : Nat) : k * m ≤ m + n ↔ (k - 1) * m ≤ n

theorem Nat.succ_mul_succ_eq (a : Nat) (b : Nat) : Nat.succ a * Nat.succ b = a * b + a + b + 1

theorem Nat.mul_self_sub_mul_self_eq (a : Nat) (b : Nat) : a * a - b * b = (a + b) * (a - b)

div/mod

theorem Nat.mod_add_div (m : Nat) (k : Nat) : m % k + k * (m / k) = m

@[simp]

theorem Nat.div_one (n : Nat) : n / 1 = n

@[simp]

theorem Nat.div_zero (n : Nat) : n / 0 = 0

@[simp]

theorem Nat.zero_div (b : Nat) : 0 / b = 0

theorem Nat.le_div_iff_mul_le {k : Nat} {x : Nat} {y : Nat} (k0 : 0 < k) : x ≤ y / k ↔ x * k ≤ y

theorem Nat.div_le_of_le_mul {m : Nat} {n : Nat} {k : Nat} : m ≤ k * n → m / k ≤ n

theorem Nat.div_eq_sub_div {b : Nat} {a : Nat} (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1

theorem Nat.div_eq_of_lt {a : Nat} {b : Nat} (h₀ : a < b) : a / b = 0

theorem Nat.div_lt_iff_lt_mul {k : Nat} {x : Nat} {y : Nat} (Hk : 0 < k) : x / k < y ↔ x < y * k

theorem Nat.sub_mul_div (x : Nat) (n : Nat) (p : Nat) (h₁ : n * p ≤ x) : (x - n * p) / n = x / n - p

theorem Nat.div_mul_le_self (m : Nat) (n : Nat) : m / n * n ≤ m

@[simp]

theorem Nat.add_div_right (x : Nat) {z : Nat} (H : 0 < z) : (x + z) / z = Nat.succ (x / z)

@[simp]

theorem Nat.add_div_left (x : Nat) {z : Nat} (H : 0 < z) : (z + x) / z = Nat.succ (x / z)

@[simp]

theorem Nat.mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n

@[simp]

theorem Nat.mul_div_left (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m

theorem Nat.div_self {n : Nat} (H : 0 < n) : n / n = 1

theorem Nat.add_mul_div_left (x : Nat) (z : Nat) {y : Nat} (H : 0 < y) : (x + y * z) / y = x / y + z

theorem Nat.add_mul_div_right (x : Nat) (y : Nat) {z : Nat} (H : 0 < z) : (x + y * z) / z = x / z + y

theorem Nat.mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m

theorem Nat.mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) : n * m / n = m

theorem Nat.div_eq_of_eq_mul_left {n : Nat} {m : Nat} {k : Nat} (H1 : 0 < n) (H2 : m = k * n) : m / n = k

theorem Nat.div_eq_of_eq_mul_right {n : Nat} {m : Nat} {k : Nat} (H1 : 0 < n) (H2 : m = n * k) : m / n = k

theorem Nat.div_eq_of_lt_le {k : Nat} {n : Nat} {m : Nat} (lo : k * n ≤ m) (hi : m < Nat.succ k * n) : m / n = k

theorem Nat.mul_sub_div (x : Nat) (n : Nat) (p : Nat) (h₁ : x < n * p) : (n * p - Nat.succ x) / n = p - Nat.succ (x / n)

theorem Nat.div_div_eq_div_mul (m : Nat) (n : Nat) (k : Nat) : m / n / k = m / (n * k)

theorem Nat.mul_div_mul_left {m : Nat} (n : Nat) (k : Nat) (H : 0 < m) : m * n / (m * k) = n / k

theorem Nat.mul_div_mul_right {m : Nat} (n : Nat) (k : Nat) (H : 0 < m) : n * m / (k * m) = n / k

theorem Nat.mul_div_le (m : Nat) (n : Nat) : n * (m / n) ≤ m

theorem Nat.mod_two_eq_zero_or_one (n : Nat) : n % 2 = 0 ∨ n % 2 = 1

theorem Nat.le_of_mod_lt {a : Nat} {b : Nat} (h : a % b < a) : b ≤ a

@[simp]

theorem Nat.add_mod_right (x : Nat) (z : Nat) : (x + z) % z = x % z

@[simp]

theorem Nat.add_mod_left (x : Nat) (z : Nat) : (x + z) % x = z % x

@[simp]

theorem Nat.add_mul_mod_self_left (x : Nat) (y : Nat) (z : Nat) : (x + y * z) % y = x % y

@[simp]

theorem Nat.add_mul_mod_self_right (x : Nat) (y : Nat) (z : Nat) : (x + y * z) % z = x % z

@[simp]

theorem Nat.mul_mod_right (m : Nat) (n : Nat) : m * n % m = 0

@[simp]

theorem Nat.mul_mod_left (m : Nat) (n : Nat) : m * n % n = 0

theorem Nat.mul_mod_mul_left (z : Nat) (x : Nat) (y : Nat) : z * x % (z * y) = z * (x % y)

theorem Nat.mul_mod_mul_right (z : Nat) (x : Nat) (y : Nat) : x * z % (y * z) = x % y * z

theorem Nat.sub_mul_mod {x : Nat} {k : Nat} {n : Nat} (h₁ : n * k ≤ x) : (x - n * k) % n = x % n

@[simp]

theorem Nat.mod_mod (a : Nat) (n : Nat) : a % n % n = a % n

theorem Nat.mul_mod (a : Nat) (b : Nat) (n : Nat) : a * b % n = a % n * (b % n) % n

@[simp]

theorem Nat.mod_add_mod (m : Nat) (n : Nat) (k : Nat) : (m % n + k) % n = (m + k) % n

@[simp]

theorem Nat.add_mod_mod (m : Nat) (n : Nat) (k : Nat) : (m + n % k) % k = (m + n) % k

theorem Nat.add_mod (a : Nat) (b : Nat) (n : Nat) : (a + b) % n = (a % n + b % n) % n

pow

theorem Nat.pow_succ' {m : Nat} {n : Nat} : m ^ Nat.succ n = m * m ^ n

@[simp]

theorem Nat.pow_eq {m : Nat} {n : Nat} : Nat.pow m n = m ^ n

theorem Nat.shiftLeft_eq (a : Nat) (b : Nat) : a <<< b = a * 2 ^ b

theorem Nat.one_shiftLeft (n : Nat) : 1 <<< n = 2 ^ n

theorem Nat.zero_pow {n : Nat} (H : 0 < n) : 0 ^ n = 0

@[simp]

theorem Nat.one_pow (n : Nat) : 1 ^ n = 1

@[simp]

theorem Nat.pow_one (a : Nat) : a ^ 1 = a

theorem Nat.pow_two (a : Nat) : a ^ 2 = a * a

theorem Nat.pow_add (a : Nat) (m : Nat) (n : Nat) : a ^ (m + n) = a ^ m * a ^ n

theorem Nat.pow_add' (a : Nat) (m : Nat) (n : Nat) : a ^ (m + n) = a ^ n * a ^ m

theorem Nat.pow_mul (a : Nat) (m : Nat) (n : Nat) : a ^ (m * n) = (a ^ m) ^ n

theorem Nat.pow_mul' (a : Nat) (m : Nat) (n : Nat) : a ^ (m * n) = (a ^ n) ^ m

theorem Nat.pow_right_comm (a : Nat) (m : Nat) (n : Nat) : (a ^ m) ^ n = (a ^ n) ^ m

theorem Nat.mul_pow (a : Nat) (b : Nat) (n : Nat) : (a * b) ^ n = a ^ n * b ^ n

log2

theorem Nat.le_log2 {n : Nat} {k : Nat} (h : n ≠ 0) : k ≤ Nat.log2 n ↔ 2 ^ k ≤ n

theorem Nat.log2_lt {n : Nat} {k : Nat} (h : n ≠ 0) : Nat.log2 n < k ↔ n < 2 ^ k

theorem Nat.log2_self_le {n : Nat} (h : n ≠ 0) : 2 ^ Nat.log2 n ≤ n

theorem Nat.lt_log2_self {n : Nat} : n < 2 ^ (Nat.log2 n + 1)

dvd

theorem Nat.dvd_refl (a : Nat) : a ∣ a

theorem Nat.dvd_zero (a : Nat) : a ∣ 0

theorem Nat.dvd_mul_left (a : Nat) (b : Nat) : a ∣ b * a

theorem Nat.dvd_mul_right (a : Nat) (b : Nat) : a ∣ a * b

theorem Nat.dvd_trans {a : Nat} {b : Nat} {c : Nat} (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c

theorem Nat.eq_zero_of_zero_dvd {a : Nat} (h : 0 ∣ a) : a = 0

@[simp]

theorem Nat.zero_dvd {n : Nat} : 0 ∣ n ↔ n = 0

theorem Nat.dvd_add {a : Nat} {b : Nat} {c : Nat} (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c

theorem Nat.dvd_add_iff_right {k : Nat} {m : Nat} {n : Nat} (h : k ∣ m) : k ∣ n ↔ k ∣ m + n

theorem Nat.dvd_add_iff_left {k : Nat} {m : Nat} {n : Nat} (h : k ∣ n) : k ∣ m ↔ k ∣ m + n

theorem Nat.dvd_sub {k : Nat} {m : Nat} {n : Nat} (H : n ≤ m) (h₁ : k ∣ m) (h₂ : k ∣ n) : k ∣ m - n

theorem Nat.mul_dvd_mul {a : Nat} {b : Nat} {c : Nat} {d : Nat} : a ∣ b → c ∣ d → a * c ∣ b * d

theorem Nat.mul_dvd_mul_left {b : Nat} {c : Nat} (a : Nat) (h : b ∣ c) : a * b ∣ a * c

theorem Nat.mul_dvd_mul_right {a : Nat} {b : Nat} (h : a ∣ b) (c : Nat) : a * c ∣ b * c

theorem Nat.dvd_mod_iff {k : Nat} {m : Nat} {n : Nat} (h : k ∣ n) : k ∣ m % n ↔ k ∣ m

theorem Nat.le_of_dvd {m : Nat} {n : Nat} (h : 0 < n) : m ∣ n → m ≤ n

theorem Nat.dvd_antisymm {m : Nat} {n : Nat} : m ∣ n → n ∣ m → m = n

theorem Nat.pos_of_dvd_of_pos {m : Nat} {n : Nat} (H1 : m ∣ n) (H2 : 0 < n) : 0 < m

@[simp]

theorem Nat.one_dvd (n : Nat) : 1 ∣ n

theorem Nat.eq_one_of_dvd_one {n : Nat} (H : n ∣ 1) : n = 1

@[simp]

theorem Nat.dvd_one {n : Nat} : n ∣ 1 ↔ n = 1

theorem Nat.dvd_of_mod_eq_zero {m : Nat} {n : Nat} (H : n % m = 0) : m ∣ n

theorem Nat.mod_eq_zero_of_dvd {m : Nat} {n : Nat} (H : m ∣ n) : n % m = 0

theorem Nat.dvd_iff_mod_eq_zero (m : Nat) (n : Nat) : m ∣ n ↔ n % m = 0

theorem Nat.emod_pos_of_not_dvd {a : Nat} {b : Nat} (h : ¬a ∣ b) : 0 < b % a

instance Nat.decidable_dvd : DecidableRel fun (x x_1 : Nat) => x ∣ x_1

Equations

• Nat.decidable_dvd x✝ x = decidable_of_decidable_of_iff (_ : x % x✝ = 0 ↔ x✝ ∣ x)

theorem Nat.mul_div_cancel' {n : Nat} {m : Nat} (H : n ∣ m) : n * (m / n) = m

theorem Nat.div_mul_cancel {n : Nat} {m : Nat} (H : n ∣ m) : m / n * n = m

theorem Nat.mul_div_assoc {k : Nat} {n : Nat} (m : Nat) (H : k ∣ n) : m * n / k = m * (n / k)

theorem Nat.dvd_of_mul_dvd_mul_left {k : Nat} {m : Nat} {n : Nat} (kpos : 0 < k) (H : k * m ∣ k * n) : m ∣ n

theorem Nat.dvd_of_mul_dvd_mul_right {k : Nat} {m : Nat} {n : Nat} (kpos : 0 < k) (H : m * k ∣ n * k) : m ∣ n

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₂

shiftLeft and shiftRight

@[simp]

theorem Nat.shiftLeft_zero {n : Nat} : n <<< 0 = n

theorem Nat.shiftLeft_succ_inside (m : Nat) (n : Nat) : m <<< (n + 1) = (2 * m) <<< n

Shiftleft on successor with multiple moved inside.

theorem Nat.shiftLeft_succ (m : Nat) (n : Nat) : m <<< (n + 1) = 2 * m <<< n

Shiftleft on successor with multiple moved to outside.

@[simp]

theorem Nat.shiftRight_zero {n : Nat} : n >>> 0 = n

theorem Nat.shiftRight_succ (m : Nat) (n : Nat) : m >>> (n + 1) = m >>> n / 2

theorem Nat.shiftRight_succ_inside (m : Nat) (n : Nat) : m >>> (n + 1) = (m / 2) >>> n

Shiftright on successor with division moved inside.

@[simp]

theorem Nat.zero_shiftLeft (n : Nat) : 0 <<< n = 0

@[simp]

theorem Nat.zero_shiftRight (n : Nat) : 0 >>> n = 0

theorem Nat.shiftRight_add (m : Nat) (n : Nat) (k : Nat) : m >>> (n + k) = m >>> n >>> k

theorem Nat.shiftLeft_shiftLeft (m : Nat) (n : Nat) (k : Nat) : m <<< n <<< k = m <<< (n + k)

theorem Nat.shiftRight_eq_div_pow (m : Nat) (n : Nat) : m >>> n = m / 2 ^ n

theorem Nat.mul_add_div {m : Nat} (m_pos : m > 0) (x : Nat) (y : Nat) : (m * x + y) / m = x + y / m

theorem Nat.mul_add_mod (m : Nat) (x : Nat) (y : Nat) : (m * x + y) % m = y % m

@[simp]

theorem Nat.mod_div_self (m : Nat) (n : Nat) : m % n / n = 0

Decidability of predicates

instance Nat.decidableBallLT (n : Nat) (P : (k : Nat) → k < n → Prop) [(n_1 : Nat) → (h : n_1 < n) → Decidable (P n_1 h)] : Decidable (∀ (n_1 : Nat) (h : n_1 < n), P n_1 h)

Equations

• One or more equations did not get rendered due to their size.
• Nat.decidableBallLT 0 x_3 = isTrue (_ : ∀ (x : Nat) (x_1 : x < 0), x_3 x x_1)

instance Nat.decidableForallFin {n : Nat} (P : Fin n → Prop) [DecidablePred P] : Decidable (∀ (i : Fin n), P i)

Equations

• Nat.decidableForallFin P = decidable_of_iff (∀ (k : Nat) (h : k < n), P { val := k, isLt := h }) (_ : (∀ (k : Nat) (h : k < n), P { val := k, isLt := h }) ↔ ∀ (i : Fin n), P i)

instance Nat.decidableBallLE (n : Nat) (P : (k : Nat) → k ≤ n → Prop) [(n_1 : Nat) → (h : n_1 ≤ n) → Decidable (P n_1 h)] : Decidable (∀ (n_1 : Nat) (h : n_1 ≤ n), P n_1 h)

Equations

• One or more equations did not get rendered due to their size.

instance Nat.decidableExistsLT {p : Nat → Prop} [h : DecidablePred p] : DecidablePred fun (n : Nat) => ∃ (m : Nat), m < n ∧ p m

Equations

• Nat.decidableExistsLT 0 = isFalse (_ : ¬∃ (x : Nat), x < 0 ∧ p x)
• Nat.decidableExistsLT (Nat.succ n) = decidable_of_decidable_of_iff (_ : (∃ (m : Nat), m < n ∧ p m) ∨ p n ↔ ∃ (x : Nat), x < Nat.succ n ∧ p x)

instance Nat.decidableExistsLE {p : Nat → Prop} [DecidablePred p] : DecidablePred fun (n : Nat) => ∃ (m : Nat), m ≤ n ∧ p m

Equations

• Nat.decidableExistsLE n = decidable_of_iff (∃ (m : Nat), m < n + 1 ∧ p m) (_ : (∃ (a : Nat), a < n + 1 ∧ p a) ↔ ∃ (a : Nat), a ≤ n ∧ p a)