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

@[deprecated Nat.succ_ne_succ_iff (since := "2025-10-26")]

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

@[deprecated Nat.succ_le_iff (since := "2025-10-26")]

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

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

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

@[simp]

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

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_self_ne_one (n : Nat) : n + n ≠ 1

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

@[deprecated Nat.add_eq_zero_iff (since := "2025-10-26")]

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

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

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

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

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

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

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

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

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

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

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

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.div_pow_of_pos (a n : Nat) : n > 0 → a ∣ 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

theorem Nat.log2_eq_iff {n k : Nat} (h : n ≠ 0) : n.log2 = k ↔ 2 ^ k ≤ n ∧ n < 2 ^ (k + 1)

theorem Nat.log2_two_mul {n : Nat} (h : n ≠ 0) : (2 * n).log2 = n.log2 + 1

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

Shift left on successor with multiple moved inside.

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

Shift left on successor with multiple moved to outside.

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

Shift right 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

theorem Nat.lt_mul_div_self_add {x k : Nat} (h : 0 < k) : x < k * (x / k) + k

theorem Nat.mul_sub_mod {x n p : Nat} (h : x < n * p) : (n * p - (x + 1)) % n = n - (x % n + 1)

Decidability of predicates

@[implicit_reducible]

noncomputable 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 ⋯

Tail-recursive runtime replacements for the bounded-quantifier decision procedures

decidableBallLT, decidableExistsLT, and decidableExistsLT' recurse to depth n in non-tail position, so running the compiled instance is either quadratic (decidableBallLT rebuilds the predicate at every level) or overflows the stack for large n. Each is replaced at runtime by a proven-equivalent tail-recursive version via @[csimp]; kernel reduction (by decide) is unaffected, as it uses the original structural definitions.

The roots are marked noncomputable so the non-tail-recursive code is never compiled at all, and each @[csimp] replacement is registered immediately after its root and before the Fin/≤ wrappers (decidableForallFin, decidableExistsFin, decidableBall/ExistsLE, …). The wrappers reduce to these roots through @[inline] decidable_of_iff, so they pick up the tail-recursive versions; and because the roots are noncomputable, a wrapper placed before its replacement fails to compile rather than silently regressing.

@[inline]

def Nat.allLTTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool

Tail-recursive Bool loop: true iff f i h holds for every i < n (short-circuits on the first false). Used at runtime by decidableBallLT via @[csimp].

Equations

• n.allLTTR f = Nat.allLTTR.loop✝ n f n ⋯

theorem Nat.allLTTR_eq_true {n : Nat} {f : (i : Nat) → i < n → Bool} : n.allLTTR f = true ↔ ∀ (i : Nat) (h : i < n), f i h = true

@[inline]

def Nat.anyLTTR (n : Nat) (f : (i : Nat) → i < n → Bool) : Bool

Tail-recursive Bool loop: true iff f i h holds for some i < n (short-circuits on the first true). Used at runtime by decidableExistsLT/' via @[csimp].

Equations

• n.anyLTTR f = Nat.anyLTTR.loop✝ n f n ⋯

theorem Nat.anyLTTR_eq_true {n : Nat} {f : (i : Nat) → i < n → Bool} : n.anyLTTR f = true ↔ ∃ (i : Nat), ∃ (h : i < n), f i h = true

def Nat.decidableBallLTTR (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)

Tail-recursive runtime replacement for decidableBallLT.

Equations

• n.decidableBallLTTR P = decidable_of_iff ((n.allLTTR fun (i : Nat) (h : i < n) => decide (P i h)) = true) ⋯

@[csimp]

theorem Nat.decidableBallLT_eq_decidableBallLTTR : decidableBallLT = decidableBallLTTR

@[implicit_reducible]

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⟩) ⋯

@[implicit_reducible]

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 ⋯) ⋯

@[implicit_reducible]

noncomputable 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 ⋯

def Nat.decidableExistsLTTR {p : Nat → Prop} [DecidablePred p] (n : Nat) : Decidable (∃ (m : Nat), m < n ∧ p m)

Tail-recursive runtime replacement for decidableExistsLT.

Equations

• n.decidableExistsLTTR = decidable_of_iff ((n.anyLTTR fun (i : Nat) (x : i < n) => decide (p i)) = true) ⋯

@[csimp]

theorem Nat.decidableExistsLT_eq_decidableExistsLTTR : @decidableExistsLT = @decidableExistsLTTR

@[implicit_reducible]

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) ⋯

@[implicit_reducible]

noncomputable 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 ⋯) ⋯

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

Tail-recursive runtime replacement for decidableExistsLT'.

Equations

• Nat.decidableExistsLT'TR = decidable_of_iff ((k.anyLTTR fun (i : Nat) (h : i < k) => decide (p i h)) = true) ⋯

@[csimp]

theorem Nat.decidableExistsLT'_eq_decidableExistsLT'TR : @decidableExistsLT' = @decidableExistsLT'TR

@[implicit_reducible]

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 ⋯) ⋯

@[implicit_reducible]

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

Equations

• Nat.decidableExistsFin P = decidable_of_iff (∃ (k : Nat), k < n ∧ ∀ (h : k < n), P ⟨k, h⟩) ⋯