Basic theorems about natural numbers

The primary purpose of the theorems in this file is to assist with reasoning about sizes of objects, array indices and such.

The content of this file was upstreamed from Batteries and mathlib, and later these theorems should be organised into other files more systematically.

@[simp]

theorem Nat.exists_ne_zero {P : Nat → Prop} : (∃ (n : Nat), ¬n = 0 ∧ P n) ↔ ∃ (n : Nat), P (n + 1)

@[simp]

theorem Nat.exists_eq_add_one {a : Nat} : (∃ (n : Nat), a = n + 1) ↔ 0 < a

@[simp]

theorem Nat.exists_add_one_eq {a : Nat} : (∃ (n : Nat), n + 1 = a) ↔ 0 < a

theorem Nat.forall_lt_succ_right' {n : Nat} {p : (m : Nat) → m < n + 1 → Prop} : (∀ (m : Nat) (h : m < n + 1), p m h) ↔ (∀ (m : Nat) (h : m < n), p m ⋯) ∧ p n ⋯

Dependent variant of forall_lt_succ_right.

theorem Nat.forall_lt_succ_right {n : Nat} {p : Nat → Prop} : (∀ (m : Nat), m < n + 1 → p m) ↔ (∀ (m : Nat), m < n → p m) ∧ p n

See forall_lt_succ_right' for a variant where p takes the bound as an argument.

theorem Nat.forall_lt_succ_left' {n : Nat} {p : (m : Nat) → m < n + 1 → Prop} : (∀ (m : Nat) (h : m < n + 1), p m h) ↔ p 0 ⋯ ∧ ∀ (m : Nat) (h : m < n), p (m + 1) ⋯

Dependent variant of forall_lt_succ_left.

theorem Nat.forall_lt_succ_left {n : Nat} {p : Nat → Prop} : (∀ (m : Nat), m < n + 1 → p m) ↔ p 0 ∧ ∀ (m : Nat), m < n → p (m + 1)

See forall_lt_succ_left' for a variant where p takes the bound as an argument.

theorem Nat.exists_lt_succ_right' {n : Nat} {p : (m : Nat) → m < n + 1 → Prop} : (∃ (m : Nat), ∃ (h : m < n + 1), p m h) ↔ (∃ (m : Nat), ∃ (h : m < n), p m ⋯) ∨ p n ⋯

Dependent variant of exists_lt_succ_right.

theorem Nat.exists_lt_succ_right {n : Nat} {p : Nat → Prop} : (∃ (m : Nat), m < n + 1 ∧ p m) ↔ (∃ (m : Nat), m < n ∧ p m) ∨ p n

See exists_lt_succ_right' for a variant where p takes the bound as an argument.

theorem Nat.exists_lt_succ_left' {n : Nat} {p : (m : Nat) → m < n + 1 → Prop} : (∃ (m : Nat), ∃ (h : m < n + 1), p m h) ↔ p 0 ⋯ ∨ ∃ (m : Nat), ∃ (h : m < n), p (m + 1) ⋯

Dependent variant of exists_lt_succ_left.

theorem Nat.exists_lt_succ_left {n : Nat} {p : Nat → Prop} : (∃ (m : Nat), m < n + 1 ∧ p m) ↔ p 0 ∨ ∃ (m : Nat), m < n ∧ p (m + 1)

See exists_lt_succ_left' for a variant where p takes the bound as an argument.

succ/pred

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

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

theorem Nat.succ_ne_succ {m n : Nat} : m.succ ≠ n.succ ↔ m ≠ n

theorem Nat.one_lt_succ_succ (n : Nat) : 1 < n.succ.succ

theorem Nat.not_succ_lt_self {n : Nat} : ¬n.succ < n

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

theorem Nat.le_succ_iff {m n : Nat} : m ≤ n.succ ↔ m ≤ n ∨ m = n.succ

theorem Nat.lt_iff_le_pred {m n : Nat} : 0 < n → (m < n ↔ m ≤ n - 1)

theorem Nat.le_of_pred_lt {n : Nat} {m : Nat} : m.pred < n → m ≤ n

theorem Nat.lt_iff_add_one_le {m n : Nat} : m < n ↔ m + 1 ≤ n

theorem Nat.lt_one_add_iff {m n : Nat} : m < 1 + n ↔ m ≤ n

theorem Nat.one_add_le_iff {m n : Nat} : 1 + m ≤ n ↔ m < n

theorem Nat.one_le_iff_ne_zero {n : Nat} : 1 ≤ n ↔ n ≠ 0

theorem Nat.one_lt_iff_ne_zero_and_ne_one {n : Nat} : 1 < n ↔ n ≠ 0 ∧ n ≠ 1

theorem Nat.le_one_iff_eq_zero_or_eq_one {n : Nat} : n ≤ 1 ↔ n = 0 ∨ n = 1

theorem Nat.one_le_of_lt {a b : Nat} (h : a < b) : 1 ≤ b

theorem Nat.pred_one_add (n : Nat) : (1 + n).pred = n

theorem Nat.pred_eq_self_iff {n : Nat} : n.pred = n ↔ n = 0

theorem Nat.pred_eq_of_eq_succ {m n : Nat} (H : m = n.succ) : m.pred = n

@[simp]

theorem Nat.pred_eq_succ_iff {n m : Nat} : n - 1 = m + 1 ↔ n = m + 2

@[simp]

theorem Nat.add_succ_sub_one (m n : Nat) : m + n.succ - 1 = m + n

@[simp]

theorem Nat.succ_add_sub_one (n m : Nat) : m.succ + n - 1 = m + n

theorem Nat.pred_sub (n m : Nat) : n.pred - m = (n - m).pred

theorem Nat.self_add_sub_one (n : Nat) : n + (n - 1) = 2 * n - 1

theorem Nat.sub_one_add_self (n : Nat) : n - 1 + n = 2 * n - 1

theorem Nat.self_add_pred (n : Nat) : n + n.pred = (2 * n).pred

theorem Nat.pred_add_self (n : Nat) : n.pred + n = (2 * n).pred

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

theorem Nat.lt_of_lt_pred {m n : Nat} (h : m < n - 1) : m < n

theorem Nat.le_add_pred_of_pos {b : Nat} (a : Nat) (hb : b ≠ 0) : a ≤ b + (a - 1)

theorem Nat.lt_pred_iff {a : Nat} {b : Nat} : a < b.pred ↔ a.succ < b

add

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

theorem Nat.add_eq_left {a b : Nat} : a + b = a ↔ b = 0

@[simp]

theorem Nat.add_eq_right {a b : Nat} : a + b = b ↔ a = 0

@[simp]

theorem Nat.left_eq_add {a b : Nat} : a = a + b ↔ b = 0

@[simp]

theorem Nat.right_eq_add {a b : Nat} : b = a + b ↔ a = 0

@[deprecated Nat.add_eq_right (since := "2025-04-15")]

theorem Nat.add_left_eq_self {a b : Nat} : a + b = b ↔ a = 0

@[deprecated Nat.add_eq_left (since := "2025-04-15")]

theorem Nat.add_right_eq_self {a b : Nat} : a + b = a ↔ b = 0

@[deprecated Nat.left_eq_add (since := "2025-04-15")]

theorem Nat.self_eq_add_right {a b : Nat} : a = a + b ↔ b = 0

@[deprecated Nat.right_eq_add (since := "2025-04-15")]

theorem Nat.self_eq_add_left {a b : Nat} : a = b + a ↔ b = 0

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

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

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

@[simp]

theorem Nat.lt_add_left_iff_pos {n 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

theorem Nat.le_iff_lt_add_one {x y : Nat} : x ≤ y ↔ x < y + 1

@[simp]

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

theorem Nat.add_pos_iff_pos_or_pos {m n : Nat} : 0 < m + n ↔ 0 < m ∨ 0 < n

theorem Nat.add_eq_one_iff {m n : Nat} : m + n = 1 ↔ m = 0 ∧ n = 1 ∨ m = 1 ∧ n = 0

theorem Nat.add_eq_two_iff {m n : Nat} : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0

theorem Nat.add_eq_three_iff {m n : Nat} : m + n = 3 ↔ m = 0 ∧ n = 3 ∨ m = 1 ∧ n = 2 ∨ m = 2 ∧ n = 1 ∨ m = 3 ∧ n = 0

theorem Nat.le_add_one_iff {m n : Nat} : m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1

theorem Nat.le_and_le_add_one_iff {n m : Nat} : n ≤ m ∧ m ≤ n + 1 ↔ m = n ∨ m = n + 1

theorem Nat.add_succ_lt_add {a b c d : Nat} (hab : a < b) (hcd : c < d) : a + c + 1 < b + d

theorem Nat.le_or_le_of_add_eq_add_pred {a c b d : Nat} (h : a + c = b + d - 1) : b ≤ a ∨ d ≤ c

sub

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

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

theorem Nat.add_sub_sub_add_right (n m k l : Nat) : n + l - m - (k + l) = n - m - k

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

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

@[simp]

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

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

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

theorem Nat.sub_sub_self {n m : Nat} (h : m ≤ n) : n - (n - m) = m

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

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

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

@[simp]

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

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

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

theorem Nat.add_lt_iff_lt_sub_right {a b c : Nat} : a + b < c ↔ a < c - b

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

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

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

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

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

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

@[reducible, inline]

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

Equations

• @Nat.sub_lt_self = @Nat.sub_lt_of_pos_le

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

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

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

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

theorem Nat.sub_lt_add_one (a b : Nat) : a - b < a + 1

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

theorem Nat.exists_eq_add_of_le {m n : Nat} (h : m ≤ n) : ∃ (k : Nat), n = m + k

theorem Nat.exists_eq_add_of_le' {m n : Nat} (h : m ≤ n) : ∃ (k : Nat), n = k + m

theorem Nat.exists_eq_add_of_lt {m n : Nat} (h : m < n) : ∃ (k : Nat), n = m + k + 1

theorem Nat.sub_succ' (m n : Nat) : m - n.succ = m - n - 1

A version of Nat.sub_succ in the form _ - 1 instead of Nat.pred _.

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

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

theorem Nat.eq_sub_of_add_eq' {a b c : Nat} (h : b + c = a) : c = a - b

theorem Nat.lt_sub_iff_add_lt {a b c : Nat} : a < c - b ↔ a + b < c

theorem Nat.lt_sub_iff_add_lt' {a b c : Nat} : a < c - b ↔ b + a < c

theorem Nat.sub_lt_iff_lt_add {a b c : Nat} (hba : b ≤ a) : a - b < c ↔ a < c + b

theorem Nat.sub_lt_iff_lt_add' {a b c : Nat} (hba : b ≤ a) : a - b < c ↔ a < b + c

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

theorem Nat.add_sub_sub_cancel {a b c : Nat} (h : c ≤ a) : a + b - (a - c) = b + c

theorem Nat.sub_add_sub_cancel {a b c : Nat} (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c

theorem Nat.sub_lt_sub_iff_right {a b c : Nat} (h : c ≤ a) : a - c < b - c ↔ a < b

min/max

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

@[simp]

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

instance Nat.instIdempotentOpMin : Std.IdempotentOp min

@[simp]

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

instance Nat.instAssociativeMin : Std.Associative min

@[simp]

theorem Nat.min_self_assoc {m n : Nat} : min m (min m n) = min m n

@[simp]

theorem Nat.min_self_assoc' {m n : Nat} : min n (min m n) = min n m

@[simp]

theorem Nat.min_add_left_self {a b : Nat} : min a (b + a) = a

@[simp]

theorem Nat.min_add_right_self {a b : Nat} : min a (a + b) = a

@[simp]

theorem Nat.add_left_min_self {a b : Nat} : min (b + a) a = a

@[simp]

theorem Nat.add_right_min_self {a b : Nat} : min (a + b) a = a

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

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

@[simp]

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

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

@[simp]

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

instance Nat.instIdempotentOpMax : Std.IdempotentOp max

instance Nat.instLawfulIdentityMaxOfNat : Std.LawfulIdentity max 0

@[simp]

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

instance Nat.instAssociativeMax : Std.Associative max

@[simp]

theorem Nat.max_add_left_self {a b : Nat} : max a (b + a) = b + a

@[simp]

theorem Nat.max_add_right_self {a b : Nat} : max a (a + b) = a + b

@[simp]

theorem Nat.add_left_max_self {a b : Nat} : max (b + a) a = b + a

@[simp]

theorem Nat.add_right_max_self {a b : Nat} : max (a + b) a = a + b

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem Nat.min_eq_zero_iff {m n : Nat} : min m n = 0 ↔ m = 0 ∨ n = 0

@[simp]

theorem Nat.max_eq_zero_iff {m n : Nat} : max m n = 0 ↔ m = 0 ∧ n = 0

theorem Nat.add_eq_max_iff {m n : Nat} : m + n = max m n ↔ m = 0 ∨ n = 0

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

mul

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

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

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

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

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

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

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

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

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

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

theorem Nat.ne_zero_of_mul_ne_zero_right {n 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 c b 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 c b d : Nat} (hac : a < c) (hbd : b ≤ d) (hb : 0 < b) : a * b < c * d

theorem Nat.mul_lt_mul_of_le_of_lt {a c b 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 c b d : Nat} (hac : a ≤ c) (hbd : b < d) (ha : 0 < a) : a * b < c * d

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

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

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

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

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

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

theorem Nat.pos_of_mul_pos_left {a b : Nat} (h : 0 < a * b) : 0 < b

theorem Nat.pos_of_mul_pos_right {a b : Nat} (h : 0 < a * b) : 0 < a

@[simp]

theorem Nat.mul_pos_iff_of_pos_left {a b : Nat} (h : 0 < a) : 0 < a * b ↔ 0 < b

@[simp]

theorem Nat.mul_pos_iff_of_pos_right {a b : Nat} (h : 0 < b) : 0 < a * b ↔ 0 < a

theorem Nat.pos_of_lt_mul_left {a b c : Nat} (h : a < b * c) : 0 < c

theorem Nat.pos_of_lt_mul_right {a b c : Nat} (h : a < b * c) : 0 < b

theorem Nat.mul_dvd_mul_iff_left {a b c : Nat} (h : 0 < a) : a * b ∣ a * c ↔ b ∣ c

theorem Nat.mul_dvd_mul_iff_right {a b c : Nat} (h : 0 < c) : a * c ∣ b * c ↔ a ∣ b

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

theorem Nat.mul_left_inj {a b c : Nat} (ha : a ≠ 0) : b * a = c * a ↔ b = c

theorem Nat.mul_right_inj {a b c : Nat} (ha : a ≠ 0) : a * b = a * c ↔ b = c

theorem Nat.mul_ne_mul_left {a b c : Nat} (ha : a ≠ 0) : b * a ≠ c * a ↔ b ≠ c

theorem Nat.mul_ne_mul_right {a b c : Nat} (ha : a ≠ 0) : a * b ≠ a * c ↔ b ≠ c

theorem Nat.mul_eq_left {a b : Nat} (ha : a ≠ 0) : a * b = a ↔ b = 1

theorem Nat.mul_eq_right {b a : Nat} (hb : b ≠ 0) : a * b = b ↔ a = 1

theorem Nat.one_lt_mul_iff {m n : Nat} : 1 < m * n ↔ 0 < m ∧ 0 < n ∧ (1 < m ∨ 1 < n)

The product of two natural numbers is greater than 1 if and only if at least one of them is greater than 1 and both are positive.

theorem Nat.eq_one_of_mul_eq_one_right {m n : Nat} (H : m * n = 1) : m = 1

theorem Nat.eq_one_of_mul_eq_one_left {m n : Nat} (H : m * n = 1) : n = 1

@[simp]

theorem Nat.lt_mul_iff_one_lt_left {b a : Nat} (hb : 0 < b) : b < a * b ↔ 1 < a

@[simp]

theorem Nat.lt_mul_iff_one_lt_right {a b : Nat} (ha : 0 < a) : a < a * b ↔ 1 < b

theorem Nat.eq_zero_of_two_mul_le {n : Nat} (h : 2 * n ≤ n) : n = 0

theorem Nat.eq_zero_of_mul_le {n m : Nat} (hb : 2 ≤ n) (h : n * m ≤ m) : m = 0

theorem Nat.succ_mul_pos {n : Nat} (m : Nat) (hn : 0 < n) : 0 < m.succ * n

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

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

theorem Nat.lt_iff_lt_of_mul_eq_mul {a b d c e : Nat} (ha : a ≠ 0) (hbd : a = b * d) (hce : a = c * e) : c < b ↔ d < e

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

theorem Nat.mul_self_le_mul_self_iff {m n : Nat} : m * m ≤ n * n ↔ m ≤ n

theorem Nat.mul_self_lt_mul_self_iff {m n : Nat} : m * m < n * n ↔ m < n

theorem Nat.le_mul_self (n : Nat) : n ≤ n * n

theorem Nat.mul_self_inj {m n : Nat} : m * m = n * n ↔ m = n

@[simp]

theorem Nat.lt_mul_self_iff {n : Nat} : n < n * n ↔ 1 < n

theorem Nat.add_sub_one_le_mul {a b : Nat} (ha : a ≠ 0) (hb : b ≠ 0) : a + b - 1 ≤ a * b

theorem Nat.add_le_mul {a : Nat} (ha : 2 ≤ a) {b : Nat} : 2 ≤ b → a + b ≤ a * b

div/mod

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

@[simp]

theorem Nat.mod_two_bne_zero {a : Nat} : (a % 2 != 0) = (a % 2 == 1)

@[simp]

theorem Nat.mod_two_bne_one {a : Nat} : (a % 2 != 1) = (a % 2 == 0)

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem Nat.mul_mod_mod (m n l : Nat) : m * (n % l) % l = m * n % l

@[simp]

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

@[simp]

theorem Nat.mod_mul_mod (m n l : Nat) : m % l * n % l = m * n % l

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

@[simp]

theorem Nat.self_sub_mod (n k : Nat) [NeZero k] : (n - k) % n = n - k

theorem Nat.mod_eq_sub (x w : Nat) : x % w = x - w * (x / w)

theorem Nat.div_dvd_div {m n k : Nat} : k ∣ m → m ∣ n → m / k ∣ n / k

@[simp]

theorem Nat.div_dvd_iff_dvd_mul {a b c : Nat} (h : b ∣ a) (hb : 0 < b) : a / b ∣ c ↔ a ∣ b * c

theorem Nat.div_eq_self {m n : Nat} : m / n = m ↔ m = 0 ∨ n = 1

@[simp]

theorem Nat.div_eq_zero_iff {a b : Nat} : a / b = 0 ↔ b = 0 ∨ a < b

theorem Nat.div_ne_zero_iff {a b : Nat} : a / b ≠ 0 ↔ b ≠ 0 ∧ b ≤ a

@[simp]

theorem Nat.div_pos_iff {a b : Nat} : 0 < a / b ↔ 0 < b ∧ b ≤ a

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

theorem Nat.mul_div_le_mul_div_assoc (a b c : Nat) : a * (b / c) ≤ a * b / c

theorem Nat.eq_mul_of_div_eq_right {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) : a = b * c

theorem Nat.eq_mul_of_div_eq_left {a b c : Nat} (H1 : b ∣ a) (H2 : a / b = c) : a = c * b

theorem Nat.mul_div_cancel_left' {a b : Nat} (Hd : a ∣ b) : a * (b / a) = b

theorem Nat.lt_div_mul_add {a b : Nat} (hb : 0 < b) : a < a / b * b + b

@[simp]

theorem Nat.div_left_inj {a b d : Nat} (hda : d ∣ a) (hdb : d ∣ b) : a / d = b / d ↔ a = b

theorem Nat.div_le_iff_le_mul_add_pred {b a c : Nat} (hb : 0 < b) : a / b ≤ c ↔ a ≤ b * c + (b - 1)

theorem Nat.one_le_div_iff {a b : Nat} (hb : 0 < b) : 1 ≤ a / b ↔ b ≤ a

theorem Nat.div_lt_one_iff {b a : Nat} (hb : 0 < b) : a / b < 1 ↔ a < b

theorem Nat.div_le_div_right {a b c : Nat} (h : a ≤ b) : a / c ≤ b / c

theorem Nat.lt_of_div_lt_div {a b c : Nat} (h : a / c < b / c) : a < b

theorem Nat.sub_mul_div (a b c : Nat) : (a - b * c) / b = a / b - c

theorem Nat.mul_sub_div_of_dvd {b c : Nat} (hc : c ≠ 0) (hcb : c ∣ b) (a : Nat) : (c * a - b) / c = a - b / c

theorem Nat.mul_add_mul_div_of_dvd {b d a c : Nat} (hb : b ≠ 0) (hd : d ≠ 0) (hba : b ∣ a) (hdc : d ∣ c) : (a * d + b * c) / (b * d) = a / b + c / d

theorem Nat.mul_sub_mul_div_of_dvd {b d a c : Nat} (hb : b ≠ 0) (hd : d ≠ 0) (hba : b ∣ a) (hdc : d ∣ c) : (a * d - b * c) / (b * d) = a / b - c / d

theorem Nat.div_mul_right_comm {a b : Nat} (hba : b ∣ a) (c : Nat) : a / b * c = a * c / b

theorem Nat.mul_div_right_comm {a b : Nat} (hba : b ∣ a) (c : Nat) : a * c / b = a / b * c

theorem Nat.div_eq_iff_eq_mul_right {a b c : Nat} (H : 0 < b) (H' : b ∣ a) : a / b = c ↔ a = b * c

theorem Nat.div_eq_iff_eq_mul_left {a b c : Nat} (H : 0 < b) (H' : b ∣ a) : a / b = c ↔ a = c * b

theorem Nat.eq_div_iff_mul_eq_left {c b a : Nat} (hc : c ≠ 0) (hcb : c ∣ b) : a = b / c ↔ b = a * c

theorem Nat.div_mul_div_comm {a b c d : Nat} : b ∣ a → d ∣ c → a / b * (c / d) = a * c / (b * d)

theorem Nat.mul_div_mul_comm {a b c d : Nat} (hba : b ∣ a) (hdc : d ∣ c) : a * c / (b * d) = a / b * (c / d)

theorem Nat.eq_zero_of_le_div {n m : Nat} (hn : 2 ≤ n) (h : m ≤ m / n) : m = 0

theorem Nat.div_mul_div_le_div (a b c : Nat) : a / c * b / a ≤ b / c

theorem Nat.eq_zero_of_le_div_two {n : Nat} (h : n ≤ n / 2) : n = 0

theorem Nat.le_div_two_of_div_two_lt_sub {a b : Nat} (h : a / 2 < a - b) : b ≤ a / 2

theorem Nat.div_two_le_of_sub_le_div_two {a b : Nat} (h : a - b ≤ a / 2) : a / 2 ≤ b

theorem Nat.div_le_div_of_mul_le_mul {d c a b : Nat} (hd : d ≠ 0) (hdc : d ∣ c) (h : a * d ≤ c * b) : a / b ≤ c / d

theorem Nat.div_eq_sub_mod_div {m n : Nat} : m / n = (m - m % n) / n

theorem Nat.eq_div_of_mul_eq_left {c a b : Nat} (hc : c ≠ 0) (h : a * c = b) : a = b / c

theorem Nat.eq_div_of_mul_eq_right {c a b : Nat} (hc : c ≠ 0) (h : c * a = b) : a = b / c

theorem Nat.mul_le_of_le_div (k x y : Nat) (h : x ≤ y / k) : x * k ≤ y

theorem Nat.div_le_iff_le_mul_of_dvd {b a c : Nat} (hb : b ≠ 0) (hba : b ∣ a) : a / b ≤ c ↔ a ≤ c * b

theorem Nat.div_lt_div_right {a b c : Nat} (ha : a ≠ 0) : a ∣ b → a ∣ c → (b / a < c / a ↔ b < c)

theorem Nat.div_lt_div_left {a b c : Nat} (ha : a ≠ 0) (hba : b ∣ a) (hca : c ∣ a) : a / b < a / c ↔ c < b

theorem Nat.lt_div_iff_mul_lt_of_dvd {c b a : Nat} (hc : c ≠ 0) (hcb : c ∣ b) : a < b / c ↔ a * c < b

theorem Nat.div_mul_div_le (a b c d : Nat) : a / b * (c / d) ≤ a * c / (b * d)

pow

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

theorem Nat.pow_add_one' {m n : Nat} : m ^ (n + 1) = m * m ^ n

@[simp]

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

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

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

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

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

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

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

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

theorem Nat.one_lt_two_pow {n : Nat} (h : n ≠ 0) : 1 < 2 ^ n

@[simp]

theorem Nat.one_lt_two_pow_iff {n : Nat} : 1 < 2 ^ n ↔ n ≠ 0

theorem Nat.one_le_two_pow {n : Nat} : 1 ≤ 2 ^ n

@[simp]

theorem Nat.one_mod_two_pow_eq_one {n : Nat} : 1 % 2 ^ n = 1 ↔ 0 < n

@[simp]

theorem Nat.one_mod_two_pow {n : Nat} (h : 0 < n) : 1 % 2 ^ n = 1

theorem Nat.pow_lt_pow_succ {a n : Nat} (h : 1 < a) : a ^ n < a ^ (n + 1)

theorem Nat.pow_lt_pow_of_lt {a n m : Nat} (h : 1 < a) (w : n < m) : a ^ n < a ^ m

theorem Nat.pow_le_pow_of_le {a n m : Nat} (h : 1 < a) (w : n ≤ m) : a ^ n ≤ a ^ m

theorem Nat.pow_le_pow_iff_right {a n m : Nat} (h : 1 < a) : a ^ n ≤ a ^ m ↔ n ≤ m

theorem Nat.pow_lt_pow_iff_right {a n m : Nat} (h : 1 < a) : a ^ n < a ^ m ↔ n < m

@[simp]

theorem Nat.pow_pred_mul {x w : Nat} (h : 0 < w) : x ^ (w - 1) * x = x ^ w

theorem Nat.pow_pred_lt_pow {x w : Nat} (h₁ : 1 < x) (h₂ : 0 < w) : x ^ (w - 1) < x ^ w

theorem Nat.two_pow_pred_lt_two_pow {w : Nat} (h : 0 < w) : 2 ^ (w - 1) < 2 ^ w

@[simp]

theorem Nat.two_pow_pred_add_two_pow_pred {w : Nat} (h : 0 < w) : 2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ w

@[simp]

theorem Nat.two_pow_sub_two_pow_pred {w : Nat} (h : 0 < w) : 2 ^ w - 2 ^ (w - 1) = 2 ^ (w - 1)

@[simp]

theorem Nat.two_pow_pred_mod_two_pow {w : Nat} (h : 0 < w) : 2 ^ (w - 1) % 2 ^ w = 2 ^ (w - 1)

theorem Nat.pow_lt_pow_iff_pow_mul_le_pow {a n m : Nat} (h : 1 < a) : a ^ n < a ^ m ↔ a ^ n * a ≤ a ^ m

theorem Nat.lt_pow_self {n a : Nat} (h : 1 < a) : n < a ^ n

theorem Nat.lt_two_pow_self {n : Nat} : n < 2 ^ n

@[simp]

theorem Nat.mod_two_pow_self {n : Nat} : n % 2 ^ n = n

@[simp]

theorem Nat.two_pow_pred_mul_two {w : Nat} (h : 0 < w) : 2 ^ (w - 1) * 2 = 2 ^ w

theorem Nat.le_pow {a b : Nat} (h : 0 < b) : a ≤ a ^ b

theorem Nat.pow_lt_pow_right {a m n : Nat} (ha : 1 < a) (h : m < n) : a ^ m < a ^ n

theorem Nat.pow_le_pow_iff_left {a b n : Nat} (hn : n ≠ 0) : a ^ n ≤ b ^ n ↔ a ≤ b

theorem Nat.pow_lt_pow_iff_left {a b n : Nat} (hn : n ≠ 0) : a ^ n < b ^ n ↔ a < b

@[simp]

theorem Nat.pow_eq_zero {a n : Nat} : a ^ n = 0 ↔ a = 0 ∧ n ≠ 0

theorem Nat.le_self_pow {n : Nat} (hn : n ≠ 0) (a : Nat) : a ≤ a ^ n

theorem Nat.one_le_pow (n m : Nat) (h : 0 < m) : 1 ≤ m ^ n

theorem Nat.one_lt_pow {n a : Nat} (hn : n ≠ 0) (ha : 1 < a) : 1 < a ^ n

theorem Nat.two_pow_succ (n : Nat) : 2 ^ (n + 1) = 2 ^ n + 2 ^ n

theorem Nat.one_lt_pow' (n m : Nat) : 1 < (m + 2) ^ (n + 1)

@[simp]

theorem Nat.one_lt_pow_iff {n : Nat} (hn : n ≠ 0) {a : Nat} : 1 < a ^ n ↔ 1 < a

theorem Nat.one_lt_two_pow' (n : Nat) : 1 < 2 ^ (n + 1)

theorem Nat.mul_lt_mul_pow_succ {a b n : Nat} (ha : 0 < a) (hb : 1 < b) : n * b < a * b ^ (n + 1)

theorem Nat.pow_two_sub_pow_two (a b : Nat) : a ^ 2 - b ^ 2 = (a + b) * (a - b)

theorem Nat.pow_pos_iff {a n : Nat} : 0 < a ^ n ↔ 0 < a ∨ n = 0

theorem Nat.pow_self_pos {n : Nat} : 0 < n ^ n

theorem Nat.pow_self_mul_pow_self_le {m n : Nat} : m ^ m * n ^ n ≤ (m + n) ^ (m + n)

theorem Nat.pow_right_inj {a m n : Nat} (ha : 1 < a) : a ^ m = a ^ n ↔ m = n

@[simp]

theorem Nat.pow_eq_one {a n : Nat} : a ^ n = 1 ↔ a = 1 ∨ n = 0

theorem Nat.pow_eq_self_iff {a b : Nat} (ha : 1 < a) : a ^ b = a ↔ b = 1

For a > 1, a ^ b = a iff b = 1.

@[simp]

theorem Nat.pow_le_one_iff {n a : Nat} (hn : n ≠ 0) : a ^ n ≤ 1 ↔ a ≤ 1

log2

@[simp]

theorem Nat.log2_zero : log2 0 = 0

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

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

@[simp]

theorem Nat.log2_two_pow {n : Nat} : (2 ^ n).log2 = n

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

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

mod, dvd

theorem Nat.pow_dvd_pow_iff_pow_le_pow {k l x : Nat} : 0 < x → (x ^ k ∣ x ^ l ↔ x ^ k ≤ x ^ l)

theorem Nat.pow_dvd_pow_iff_le_right {x k l : Nat} (w : 1 < x) : x ^ k ∣ x ^ l ↔ k ≤ l

If 1 < x, then x^k divides x^l if and only if k is at most l.

theorem Nat.pow_dvd_pow_iff_le_right' {b k l : Nat} : (b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l

theorem Nat.pow_dvd_pow {m n : Nat} (a : Nat) (h : m ≤ n) : a ^ m ∣ a ^ n

theorem Nat.pow_sub_mul_pow (a : Nat) {m n : Nat} (h : m ≤ n) : a ^ (n - m) * a ^ m = a ^ n

theorem Nat.pow_dvd_of_le_of_pow_dvd {p m n k : Nat} (hmn : m ≤ n) (hdiv : p ^ n ∣ k) : p ^ m ∣ k

theorem Nat.dvd_of_pow_dvd {p k m : Nat} (hk : 1 ≤ k) (hpk : p ^ k ∣ m) : p ∣ m

theorem Nat.pow_div {x m n : Nat} (h : n ≤ m) (hx : 0 < x) : x ^ m / x ^ n = x ^ (m - n)

theorem Nat.div_pow {a b c : Nat} (h : a ∣ b) : (b / a) ^ c = b ^ c / a ^ c

@[simp]

theorem Nat.mod_two_not_eq_one {n : Nat} : ¬n % 2 = 1 ↔ n % 2 = 0

@[simp]

theorem Nat.mod_two_not_eq_zero {n : Nat} : ¬n % 2 = 0 ↔ n % 2 = 1

theorem Nat.mod_two_ne_one {n : Nat} : n % 2 ≠ 1 ↔ n % 2 = 0

theorem Nat.mod_two_ne_zero {n : Nat} : n % 2 ≠ 0 ↔ n % 2 = 1

theorem Nat.lt_div_iff_mul_lt' {d n : Nat} (hdn : d ∣ n) (a : Nat) : a < n / d ↔ d * a < n

Variant of Nat.lt_div_iff_mul_lt that assumes d ∣ n.

theorem Nat.mul_div_eq_iff_dvd {n d : Nat} : d * (n / d) = n ↔ d ∣ n

theorem Nat.mul_div_lt_iff_not_dvd {n d : Nat} : d * (n / d) < n ↔ ¬d ∣ n

theorem Nat.div_eq_iff_eq_of_dvd_dvd {n a b : Nat} (hn : n ≠ 0) (ha : a ∣ n) (hb : b ∣ n) : n / a = n / b ↔ a = b

theorem Nat.le_iff_ne_zero_of_dvd {a b : Nat} (ha : a ≠ 0) (hab : a ∣ b) : a ≤ b ↔ b ≠ 0

theorem Nat.div_ne_zero_iff_of_dvd {b a : Nat} (hba : b ∣ a) : a / b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0

theorem Nat.pow_mod (a b n : Nat) : a ^ b % n = (a % n) ^ b % n

theorem Nat.lt_of_pow_dvd_right {b a n : Nat} (hb : b ≠ 0) (ha : 2 ≤ a) (h : a ^ n ∣ b) : n < b

theorem Nat.div_dvd_of_dvd {n m : Nat} (h : n ∣ m) : m / n ∣ m

theorem Nat.div_div_self {n m : Nat} (h : n ∣ m) (hm : m ≠ 0) : m / (m / n) = n

theorem Nat.not_dvd_of_pos_of_lt {n m : Nat} (h1 : 0 < n) (h2 : n < m) : ¬m ∣ n

theorem Nat.eq_of_dvd_of_lt_two_mul {a b : Nat} (ha : a ≠ 0) (hdvd : b ∣ a) (hlt : a < 2 * b) : a = b

theorem Nat.mod_eq_iff_lt {n m : Nat} (hn : n ≠ 0) : m % n = m ↔ m < n

@[simp]

theorem Nat.mod_succ_eq_iff_lt {m n : Nat} : m % n.succ = m ↔ m < n.succ

@[simp]

theorem Nat.mod_succ (n : Nat) : n % n.succ = n

theorem Nat.mod_add_div' (a b : Nat) : a % b + a / b * b = a

theorem Nat.div_add_mod' (a b : Nat) : a / b * b + a % b = a

theorem Nat.div_mod_unique {b a d c : Nat} (h : 0 < b) : a / b = d ∧ a % b = c ↔ c + b * d = a ∧ c < b

See also Nat.divModEquiv for a similar statement as an Equiv.

theorem Nat.sub_mod_eq_zero_of_mod_eq {m k n : Nat} (h : m % k = n % k) : (m - n) % k = 0

If m and n are equal mod k, m - n is zero mod k.

@[simp]

theorem Nat.one_mod (n : Nat) : 1 % (n + 2) = 1

theorem Nat.one_mod_eq_one {n : Nat} : 1 % n = 1 ↔ n ≠ 1

theorem Nat.dvd_sub_mod {n : Nat} (k : Nat) : n ∣ k - k % n

theorem Nat.add_mod_eq_ite {k m n : Nat} : (m + n) % k = if k ≤ m % k + n % k then m % k + n % k - k else m % k + n % k

theorem Nat.dvd_add_left {a b c : Nat} (h : a ∣ c) : a ∣ b + c ↔ a ∣ b

theorem Nat.dvd_add_right {a b c : Nat} (h : a ∣ b) : a ∣ b + c ↔ a ∣ c

theorem Nat.add_mod_eq_add_mod_right {a d b : Nat} (c : Nat) (H : a % d = b % d) : (a + c) % d = (b + c) % d

theorem Nat.add_mod_eq_add_mod_left {a d b : Nat} (c : Nat) (H : a % d = b % d) : (c + a) % d = (c + b) % d

theorem Nat.mul_dvd_of_dvd_div {a b c : Nat} (hcb : c ∣ b) (h : a ∣ b / c) : c * a ∣ b

theorem Nat.eq_of_dvd_of_div_eq_one {a b : Nat} (hab : a ∣ b) (h : b / a = 1) : a = b

theorem Nat.eq_zero_of_dvd_of_div_eq_zero {a b : Nat} (hab : a ∣ b) (h : b / a = 0) : b = 0

theorem Nat.lt_mul_div_succ {b : Nat} (a : Nat) (hb : 0 < b) : a < b * (a / b + 1)

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

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

theorem Nat.mul_add_mod' (a b c : Nat) : (a * b + c) % b = c % b

theorem Nat.mul_add_mod_of_lt {a b c : Nat} (h : c < b) : (a * b + c) % b = c

@[simp]

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

theorem Nat.mod_eq_iff {a b c : Nat} : a % b = c ↔ b = 0 ∧ a = c ∨ c < b ∧ ∃ (k : Nat), a = b * k + c

theorem Nat.mod_eq_sub_iff {a b c : Nat} (h₁ : 0 < c) (h : c ≤ b) : a % b = b - c ↔ b ∣ a + c

theorem Nat.succ_mod_succ_eq_zero_iff {a b : Nat} : (a + 1) % (b + 1) = 0 ↔ a % (b + 1) = b

theorem Nat.dvd_iff_div_mul_eq (n d : Nat) : d ∣ n ↔ n / d * d = n

theorem Nat.dvd_iff_le_div_mul (n d : Nat) : d ∣ n ↔ n ≤ n / d * d

theorem Nat.dvd_iff_dvd_dvd (n d : Nat) : d ∣ n ↔ ∀ (k : Nat), k ∣ d → k ∣ n

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

@[simp]

theorem Nat.dvd_div_iff_mul_dvd {a b c : Nat} (hbc : c ∣ b) : a ∣ b / c ↔ c * a ∣ b

theorem Nat.dvd_mul_of_div_dvd {a b c : Nat} (h : b ∣ a) (hdiv : a / b ∣ c) : a ∣ b * c

@[simp]

theorem Nat.div_div_div_eq_div {a b c : Nat} (dvd : b ∣ a) (dvd2 : a ∣ c) : c / (a / b) / b = c / a

theorem Nat.eq_zero_of_dvd_of_lt {a b : Nat} (w : a ∣ b) (h : b < a) : b = 0

If a small natural number is divisible by a larger natural number, the small number is zero.

theorem Nat.le_of_lt_add_of_dvd {n a b : Nat} (h : a < b + n) : n ∣ a → n ∣ b → a ≤ b

theorem Nat.not_dvd_of_lt_of_lt_mul_succ {n k m : Nat} (h1 : n * k < m) (h2 : m < n * (k + 1)) : ¬n ∣ m

m is not divisible by n if it is between n * k and n * (k + 1) for some k.

theorem Nat.not_dvd_iff_lt_mul_succ (n : Nat) {a : Nat} (ha : 0 < a) : ¬a ∣ n ↔ ∃ (k : Nat), a * k < n ∧ n < a * (k + 1)

n is not divisible by a iff it is between a * k and a * (k + 1) for some k.

theorem Nat.div_lt_div_of_lt_of_dvd {a b d : Nat} (hdb : d ∣ b) (h : a < b) : a / d < b / d

shiftLeft and shiftRight

@[simp]

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

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

Shiftleft on successor with multiple moved inside.

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

Shiftleft on successor with multiple moved to outside.

theorem Nat.shiftRight_succ_inside (m 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.shiftLeft_add (m n k : Nat) : m <<< (n + k) = m <<< n <<< k

@[simp]

theorem Nat.shiftLeft_shiftRight (x n : Nat) : x <<< n >>> n = x

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 ⋯

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 ⟨k, h⟩) ⋯

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

• n.decidableBallLE P = decidable_of_iff (∀ (k : Nat) (h : k < n.succ), P k ⋯) ⋯

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

Equations

• Nat.decidableExistsLT 0 = isFalse ⋯
• n.succ.decidableExistsLT = decidable_of_decidable_of_iff ⋯

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

Equations

• n.decidableExistsLE = decidable_of_iff (∃ (m : Nat), m < n + 1 ∧ p m) ⋯

instance Nat.decidableExistsLT' {k : Nat} {p : (m : Nat) → m < k → Prop} [I : (m : Nat) → (h : m < k) → Decidable (p m h)] : Decidable (∃ (m : Nat), ∃ (h : m < k), p m h)

Dependent version of decidableExistsLT.

Equations

• Nat.decidableExistsLT' = isFalse ⋯
• Nat.decidableExistsLT' = decidable_of_iff ((∃ (m : Nat), ∃ (h : m < n), P m ⋯) ∨ P n ⋯) ⋯

instance Nat.decidableExistsLE' {k : Nat} {p : (m : Nat) → m ≤ k → Prop} [I : (m : Nat) → (h : m ≤ k) → Decidable (p m h)] : Decidable (∃ (m : Nat), ∃ (h : m ≤ k), p m h)

Dependent version of decidableExistsLE.

Equations

• Nat.decidableExistsLE' = decidable_of_iff (∃ (m : Nat), ∃ (h : m < k + 1), p m ⋯) ⋯

Results about List.sum specialized to Nat

theorem Nat.sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ (x : Nat), x ∈ l ∧ 0 < x