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.

This file was upstreamed from Std, and later these lemmas should be organised into other files more systematically.

le/lt

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

@[inline, reducible]

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

Equations

• @Nat.not_lt_of_gt = @Nat.lt_asymm

@[inline, reducible]

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

Equations

• @Nat.not_lt_of_lt = @Nat.lt_asymm

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

@[inline, reducible]

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

Equations

• @Nat.lt_iff_le_and_not_ge = @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.ne_iff_lt_or_gt {a : Nat} {b : Nat} : a ≠ b ↔ a < b ∨ b < a

@[inline, reducible]

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

Equations

• @Nat.lt_or_gt = @Nat.ne_iff_lt_or_gt

@[inline, reducible]

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

Equations

• Nat.le_or_ge = Nat.le_total

@[inline, reducible]

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

Equations

• Nat.le_or_le = Nat.le_total

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

theorem Nat.eq_of_lt_succ_of_not_lt {m : Nat} {n : Nat} (hmn : m < n + 1) (h : ¬m < n) : m = n

theorem Nat.eq_of_le_of_lt_succ {n : Nat} {m : Nat} (h₁ : n ≤ m) (h₂ : m < n + 1) : m = n

zero/one/two

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

@[inline, reducible]

abbrev Nat.one_pos : 0 < 1

Equations

• Nat.one_pos = 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_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.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

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

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

theorem Nat.eq_zero_of_add_eq_zero_right {n : Nat} {m : Nat} (h : n + m = 0) : n = 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.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

@[simp]

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_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.sub_eq_zero_iff_le {n : Nat} {m : Nat} : n - m = 0 ↔ n ≤ m

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

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_left {n : Nat} {k : Nat} {m : Nat} : n ≤ k → k - m ≤ k - n → n ≤ m

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

@[inline, reducible]

abbrev Nat.sub_lt_self {a : Nat} {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 : 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

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

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

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

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

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

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

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)

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

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

@[simp]

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

@[simp]

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

div/mod

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

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

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

@[simp]

theorem Nat.mod_mod_of_dvd {c : Nat} {b : Nat} (a : Nat) (h : c ∣ b) : a % b % c = a % c

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

@[inline, reducible]

abbrev Nat.pow_le_pow_left {n : Nat} {m : Nat} (h : n ≤ m) (i : Nat) : n ^ i ≤ m ^ i

Equations

• @Nat.pow_le_pow_left = @Nat.pow_le_pow_of_le_left

@[inline, reducible]

abbrev Nat.pow_le_pow_right {n : Nat} (hx : n > 0) {i : Nat} {j : Nat} : i ≤ j → n ^ i ≤ n ^ j

Equations

• @Nat.pow_le_pow_right = @Nat.pow_le_pow_of_le_right

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

theorem Nat.pow_pos {a : Nat} {n : Nat} (h : 0 < a) : 0 < a ^ n

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

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

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

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

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

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

@[simp]

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

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

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

theorem Nat.pow_dvd_pow_iff_le_right {x : Nat} {k : Nat} {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 : Nat} {k : Nat} {l : Nat} : (b + 2) ^ k ∣ (b + 2) ^ l ↔ k ≤ l

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

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

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

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

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

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

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

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

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 ⋯

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

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

• Nat.decidableBallLE n P = decidable_of_iff (∀ (k : Nat) (h : k < Nat.succ n), 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 ⋯
• Nat.decidableExistsLT (Nat.succ n) = decidable_of_decidable_of_iff ⋯

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