Documentation

Std.Data.Nat.Lemmas

theorem Nat.eq_zero_of_add_eq_zero_right {n : Nat} {m : Nat} :
n + m = 0n = 0
theorem Nat.eq_zero_of_add_eq_zero_left {n : Nat} {m : Nat} (h : n + m = 0) :
m = 0
theorem Nat.ne_of_gt {a : Nat} {b : Nat} (h : b < a) :
a b
theorem Nat.succ_le {n : Nat} {m : Nat} :
Nat.succ n m n < m
theorem Nat.le_of_not_le {a : Nat} {b : Nat} :
¬a bb a
theorem Nat.pos_of_ne_zero {n : Nat} :
n 00 < n
theorem Nat.pos_iff_ne_zero {n : Nat} :
0 < n n 0
theorem Nat.lt_iff_le_not_le {m : Nat} {n : Nat} :
m < n m n ¬n m
theorem Nat.lt_iff_le_and_ne {m : Nat} {n : Nat} :
m < n m n m n
@[simp]
theorem Nat.not_le {a : Nat} {b : Nat} :
¬a b b < a
@[simp]
theorem Nat.not_lt {a : Nat} {b : Nat} :
¬a < b b a
theorem Nat.pred_lt_pred {n : Nat} {m : Nat} :
n 0n < mNat.pred n < Nat.pred m
theorem Nat.add_left_cancel_iff {n : Nat} {m : Nat} {k : Nat} :
n + m = n + k m = k
theorem Nat.add_le_add_iff_le_right (k : Nat) (n : Nat) (m : Nat) :
n + k m + k n m
theorem Nat.lt_of_add_lt_add_left {k : Nat} {n : Nat} {m : Nat} (h : k + n < k + m) :
n < m
theorem Nat.lt_of_add_lt_add_right {a : Nat} {b : Nat} {c : Nat} (h : a + b < c + b) :
a < c
theorem Nat.lt_add_right (a : Nat) (b : Nat) (c : Nat) (h : a < b) :
a < b + c
theorem Nat.lt_add_of_pos_right {n : Nat} {k : Nat} (h : 0 < k) :
n < n + k
theorem Nat.lt_add_of_pos_left {n : Nat} {k : Nat} (h : 0 < k) :
n < k + n
theorem Nat.sub_lt_succ (a : Nat) (b : Nat) :
a - b < Nat.succ a
theorem Nat.sub_le_sub_right {n : Nat} {m : Nat} (h : n m) (k : Nat) :
n - k m - k
theorem Nat.add_self_ne_one (n : Nat) :
n + n 1
theorem Nat.le_of_le_of_sub_le_sub_right {n : Nat} {m : Nat} {k : Nat} :
k mn - k m - kn m
theorem Nat.sub_le_sub_right_iff {n : Nat} {m : Nat} {k : Nat} (h : k m) :
n - k m - k n m
theorem Nat.add_le_to_le_sub (x : Nat) {y : Nat} {k : Nat} (h : k y) :
x + k y x y - k
theorem Nat.sub_lt_of_pos_le (a : Nat) (b : Nat) (h₀ : 0 < a) (h₁ : a b) :
b - a < b
theorem Nat.sub_one (n : Nat) :
n - 1 = Nat.pred n
theorem Nat.le_of_sub_eq_zero {n : Nat} {m : Nat} :
n - m = 0n m
theorem Nat.eq_zero_of_nonpos (n : Nat) :
¬0 < nn = 0
theorem Nat.sub_eq_zero_iff_le {n : Nat} {m : Nat} :
n - m = 0 n m
theorem Nat.sub_eq_iff_eq_add {a : Nat} {b : Nat} {c : Nat} (ab : b a) :
a - b = c a = c + b
theorem Nat.lt_of_sub_eq_succ {m : Nat} {n : Nat} {l : Nat} (H : m - n = Nat.succ l) :
n < m
theorem Nat.min_eq_min {b : Nat} (a : Nat) :
Nat.min a b = min a b
theorem Nat.max_eq_max {b : Nat} (a : Nat) :
Nat.max a b = max a b
theorem Nat.min_comm (a : Nat) (b : Nat) :
min a b = min b a
theorem Nat.min_le_right (a : Nat) (b : Nat) :
min a b b
theorem Nat.min_le_left (a : Nat) (b : Nat) :
min a b a
theorem Nat.le_min {a : Nat} {b : Nat} {c : Nat} :
a min b c a b a c
theorem Nat.min_eq_left {a : Nat} {b : Nat} (h : a b) :
min a b = a
theorem Nat.min_eq_right {a : Nat} {b : Nat} (h : b a) :
min a b = b
theorem Nat.zero_min (a : Nat) :
min 0 a = 0
theorem Nat.min_zero (a : Nat) :
min a 0 = 0
theorem Nat.max_comm (a : Nat) (b : Nat) :
max a b = max b a
theorem Nat.le_max_left (a : Nat) (b : Nat) :
a max a b
theorem Nat.le_max_right (a : Nat) (b : Nat) :
b max a b
theorem Nat.max_le {a : Nat} {b : Nat} {c : Nat} :
max a b c a c b c
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.min_succ_succ (x : Nat) (y : Nat) :
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.mul_right_comm (n : Nat) (m : Nat) (k : Nat) :
n * m * k = n * k * m
theorem Nat.mul_two (n : Nat) :
n * 2 = n + n
theorem Nat.two_mul (n : Nat) :
2 * n = n + n
theorem Nat.mod_two_eq_zero_or_one (n : Nat) :
n % 2 = 0 n % 2 = 1
theorem Nat.mod_add_div (m : Nat) (k : Nat) :
m % k + k * (m / k) = m
@[simp]
theorem Nat.div_one (n : Nat) :
n / 1 = n
@[simp]
theorem Nat.div_zero (n : Nat) :
n / 0 = 0
@[simp]
theorem Nat.zero_div (b : Nat) :
0 / b = 0
theorem Nat.le_div_iff_mul_le {k : Nat} {x : Nat} {y : Nat} (k0 : 0 < k) :
x y / k x * k y
theorem Nat.div_le_of_le_mul {m : Nat} {n : Nat} {k : Nat} :
m k * nm / k n
theorem Nat.div_eq_sub_div {b : Nat} {a : Nat} (h₁ : 0 < b) (h₂ : b a) :
a / b = (a - b) / b + 1
theorem Nat.div_eq_of_lt {a : Nat} {b : Nat} (h₀ : a < b) :
a / b = 0
theorem Nat.div_lt_iff_lt_mul {k : Nat} {x : Nat} {y : Nat} (Hk : 0 < k) :
x / k < y x < y * k
theorem Nat.add_one_ne_zero (n : Nat) :
n + 1 0
theorem Nat.exists_eq_succ_of_ne_zero {n : Nat} (H : n 0) :
k, n = Nat.succ k
theorem Nat.succ_inj' {n : Nat} {m : Nat} :
theorem Nat.one_add (n : Nat) :
1 + n = Nat.succ n
theorem Nat.eq_zero_of_add_eq_zero {n : Nat} {m : Nat} (H : n + m = 0) :
n = 0 m = 0
theorem Nat.mul_eq_zero {n : Nat} {m : 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} (n0 : n 0) (m0 : m 0) :
n * m 0
theorem Nat.le_lt_antisymm {n : Nat} {m : Nat} (h₁ : n m) (h₂ : m < n) :
theorem Nat.lt_le_antisymm {n : Nat} {m : Nat} (h₁ : n < m) (h₂ : m n) :
theorem Nat.lt_asymm {n : Nat} {m : Nat} (h₁ : n < m) :
¬m < n
def Nat.lt_sum_ge (a : Nat) (b : Nat) :
a < b ⊕' b a

Strong case analysis on a < b ∨ b ≤ a∨ b ≤ a≤ a

Equations
def Nat.sum_trichotomy (a : Nat) (b : Nat) :
a < b ⊕' a = b ⊕' b < a

Strong case analysis on a < b ∨ a = b ∨ b < a∨ a = b ∨ b < a∨ b < a

Equations
  • One or more equations did not get rendered due to their size.
theorem Nat.lt_trichotomy (a : Nat) (b : Nat) :
a < b a = b b < a
theorem Nat.eq_or_lt_of_not_lt {a : Nat} {b : Nat} (hnlt : ¬a < b) :
a = b b < a
theorem Nat.lt_succ_of_lt {a : Nat} {b : Nat} (h : a < b) :
theorem Nat.one_pos :
0 < 1
theorem Nat.not_lt_of_le {n : Nat} {m : Nat} (h₁ : m n) :
¬n < m
theorem Nat.not_le_of_lt {n : Nat} {m : Nat} :
m < n¬n m
theorem Nat.lt_of_not_le {a : Nat} {b : Nat} :
¬a bb < a
theorem Nat.le_of_not_lt {a : Nat} {b : Nat} :
¬a < bb a
theorem Nat.le_or_le (a : Nat) (b : Nat) :
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_zero {i : Nat} :
i 0 i = 0
theorem Nat.lt_succ {m : Nat} {n : Nat} :
m < Nat.succ n m n
theorem Nat.sub_add_eq_max {a : Nat} {b : Nat} :
a - b + b = max a b
theorem Nat.sub_le_sub_left {n : Nat} {m : Nat} (k : Nat) (h : n m) :
k - m k - n
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.mul_self_sub_mul_self_eq (a : Nat) (b : Nat) :
a * a - b * b = (a + b) * (a - b)
theorem Nat.succ_mul_succ_eq (a : Nat) (b : Nat) :
Nat.succ a * Nat.succ b = a * b + a + b + 1
theorem Nat.succ_sub {m : Nat} {n : Nat} (h : n m) :
Nat.succ m - n = Nat.succ (m - n)
theorem Nat.sub_pos_of_lt {m : Nat} {n : Nat} (h : m < n) :
0 < n - m
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_one_sub_lt {i : Nat} {n : Nat} (h : i < n) :
n - 1 - i < n
theorem Nat.pred_inj {a : Nat} {b : Nat} :
0 < a0 < bNat.pred a = Nat.pred ba = b
theorem Nat.sub_lt_self {a : Nat} {b : Nat} (h₀ : 0 < a) (h₁ : a b) :
b - a < b
theorem Nat.add_sub_cancel' {n : Nat} {m : Nat} (h : m n) :
m + (n - m) = n
theorem Nat.sub_lt_sub_left {k : Nat} {m : Nat} {n : Nat} :
k < mk < nm - n < m - k
theorem Nat.sub_lt_left_of_lt_add {n : Nat} {k : Nat} {m : Nat} (H : n k) (h : k < n + m) :
k - n < m
theorem Nat.add_le_of_le_sub_left {n : Nat} {k : Nat} {m : Nat} (H : m k) (h : n k - m) :
m + n k
theorem Nat.le_sub_iff_add_le {x : Nat} {y : Nat} {k : Nat} (h : k y) :
x y - k x + k y
theorem Nat.le_pred_of_lt {m : Nat} {n : Nat} (h : m < n) :
m n - 1
theorem Nat.sub_add_lt_sub {n : Nat} {m : Nat} {k : Nat} (h₁ : m + k n) (h₂ : 0 < k) :
n - (m + k) < n - m
theorem Nat.le_of_mod_lt {a : Nat} {b : Nat} (h : a % b < a) :
b a
@[simp]
theorem Nat.add_mod_right (x : Nat) (z : Nat) :
(x + z) % z = x % z
@[simp]
theorem Nat.add_mod_left (x : Nat) (z : Nat) :
(x + z) % x = z % x
@[simp]
theorem Nat.add_mul_mod_self_left (x : Nat) (y : Nat) (z : Nat) :
(x + y * z) % y = x % y
@[simp]
theorem Nat.add_mul_mod_self_right (x : Nat) (y : Nat) (z : Nat) :
(x + y * z) % z = x % z
@[simp]
theorem Nat.mul_mod_right (m : Nat) (n : Nat) :
m * n % m = 0
@[simp]
theorem Nat.mul_mod_left (m : Nat) (n : Nat) :
m * n % n = 0
theorem Nat.mul_mod_mul_left (z : Nat) (x : Nat) (y : Nat) :
z * x % (z * y) = z * (x % y)
theorem Nat.mul_mod_mul_right (z : Nat) (x : Nat) (y : Nat) :
x * z % (y * z) = x % y * z
theorem Nat.sub_mul_mod {x : Nat} {k : Nat} {n : Nat} (h₁ : n * k x) :
(x - n * k) % n = x % n
theorem Nat.sub_mul_div (x : Nat) (n : Nat) (p : Nat) (h₁ : n * p x) :
(x - n * p) / n = x / n - p
theorem Nat.div_mul_le_self (m : Nat) (n : Nat) :
m / n * n m
@[simp]
theorem Nat.add_div_right (x : Nat) {z : Nat} (H : 0 < z) :
(x + z) / z = Nat.succ (x / z)
@[simp]
theorem Nat.add_div_left (x : Nat) {z : Nat} (H : 0 < z) :
(z + x) / z = Nat.succ (x / z)
@[simp]
theorem Nat.mul_div_right (n : Nat) {m : Nat} (H : 0 < m) :
m * n / m = n
@[simp]
theorem Nat.mul_div_left (m : Nat) {n : Nat} (H : 0 < n) :
m * n / n = m
theorem Nat.div_self {n : Nat} (H : 0 < n) :
n / n = 1
theorem Nat.add_mul_div_left (x : Nat) (z : Nat) {y : Nat} (H : 0 < y) :
(x + y * z) / y = x / y + z
theorem Nat.add_mul_div_right (x : Nat) (y : Nat) {z : Nat} (H : 0 < z) :
(x + y * z) / z = x / z + y
theorem Nat.mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) :
m * n / n = m
theorem Nat.mul_div_cancel_left (m : Nat) {n : Nat} (H : 0 < n) :
n * m / n = m
theorem Nat.div_eq_of_eq_mul_left {n : Nat} {m : Nat} {k : Nat} (H1 : 0 < n) (H2 : m = k * n) :
m / n = k
theorem Nat.div_eq_of_eq_mul_right {n : Nat} {m : Nat} {k : Nat} (H1 : 0 < n) (H2 : m = n * k) :
m / n = k
theorem Nat.div_eq_of_lt_le {k : Nat} {n : Nat} {m : Nat} (lo : k * n m) (hi : m < Nat.succ k * n) :
m / n = k
theorem Nat.mul_sub_div (x : Nat) (n : Nat) (p : Nat) (h₁ : x < n * p) :
(n * p - Nat.succ x) / n = p - Nat.succ (x / n)
theorem Nat.div_div_eq_div_mul (m : Nat) (n : Nat) (k : Nat) :
m / n / k = m / (n * k)
theorem Nat.mul_div_mul_left {m : Nat} (n : Nat) (k : Nat) (H : 0 < m) :
m * n / (m * k) = n / k
theorem Nat.mul_div_mul_right {m : Nat} (n : Nat) (k : Nat) (H : 0 < m) :
n * m / (k * m) = n / k
theorem Nat.mul_div_le (m : Nat) (n : Nat) :
n * (m / n) m
theorem Nat.dvd_refl (a : Nat) :
a a
theorem Nat.dvd_zero (a : Nat) :
a 0
theorem Nat.dvd_mul_left (a : Nat) (b : Nat) :
a b * a
theorem Nat.dvd_mul_right (a : Nat) (b : Nat) :
a a * b
theorem Nat.dvd_trans {a : Nat} {b : Nat} {c : Nat} (h₁ : a b) (h₂ : b c) :
a c
theorem Nat.eq_zero_of_zero_dvd {a : Nat} (h : 0 a) :
a = 0
theorem Nat.dvd_add {a : Nat} {b : Nat} {c : Nat} (h₁ : a b) (h₂ : a c) :
a b + c
theorem Nat.dvd_add_iff_right {k : Nat} {m : Nat} {n : Nat} (h : k m) :
k n k m + n
theorem Nat.dvd_add_iff_left {k : Nat} {m : Nat} {n : Nat} (h : k n) :
k m k m + n
theorem Nat.dvd_sub {k : Nat} {m : Nat} {n : Nat} (H : n m) (h₁ : k m) (h₂ : k n) :
k m - n
theorem Nat.mul_dvd_mul {a : Nat} {b : Nat} {c : Nat} {d : Nat} :
a bc da * c b * d
theorem Nat.mul_dvd_mul_left {b : Nat} {c : Nat} (a : Nat) (h : b c) :
a * b a * c
theorem Nat.mul_dvd_mul_right {a : Nat} {b : Nat} (h : a b) (c : Nat) :
a * c b * c
theorem Nat.dvd_mod_iff {k : Nat} {m : Nat} {n : Nat} (h : k n) :
k m % n k m
theorem Nat.le_of_dvd {m : Nat} {n : Nat} (h : 0 < n) :
m nm n
theorem Nat.dvd_antisymm {m : Nat} {n : Nat} :
m nn mm = n
theorem Nat.pos_of_dvd_of_pos {m : Nat} {n : Nat} (H1 : m n) (H2 : 0 < n) :
0 < m
theorem Nat.eq_one_of_dvd_one {n : Nat} (H : n 1) :
n = 1
theorem Nat.dvd_of_mod_eq_zero {m : Nat} {n : Nat} (H : n % m = 0) :
m n
theorem Nat.mod_eq_zero_of_dvd {m : Nat} {n : Nat} (H : m n) :
n % m = 0
theorem Nat.dvd_iff_mod_eq_zero (m : Nat) (n : Nat) :
m n n % m = 0
instance Nat.decidable_dvd :
DecidableRel fun x x_1 => x x_1
Equations
theorem Nat.mul_div_cancel' {n : Nat} {m : Nat} (H : n m) :
n * (m / n) = m
theorem Nat.div_mul_cancel {n : Nat} {m : Nat} (H : n m) :
m / n * n = m
theorem Nat.mul_div_assoc {k : Nat} {n : Nat} (m : Nat) (H : k n) :
m * n / k = m * (n / k)
theorem Nat.dvd_of_mul_dvd_mul_left {k : Nat} {m : Nat} {n : Nat} (kpos : 0 < k) (H : k * m k * n) :
m n
theorem Nat.dvd_of_mul_dvd_mul_right {k : Nat} {m : Nat} {n : Nat} (kpos : 0 < k) (H : m * k n * k) :
m n
theorem Nat.mul_le_mul_of_nonneg_left {a : Nat} {b : Nat} {c : Nat} (h₁ : a b) :
c * a c * b
theorem Nat.mul_le_mul_of_nonneg_right {a : Nat} {b : Nat} {c : Nat} (h₁ : a b) :
a * c b * c
theorem Nat.mul_lt_mul {a : Nat} {c : Nat} {b : Nat} {d : Nat} (hac : a < c) (hbd : b d) (pos_b : 0 < b) :
a * b < c * d
theorem Nat.mul_lt_mul' {a : Nat} {c : Nat} {b : Nat} {d : Nat} (h1 : a c) (h2 : b < d) (h3 : 0 < c) :
a * b < c * d
@[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
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
@[simp]
theorem Nat.shiftLeft_eq (a : Nat) (b : Nat) :
a <<< b = a * 2 ^ b
theorem Nat.one_shiftLeft (n : Nat) :
1 <<< n = 2 ^ n

log2 #

theorem Nat.le_log2 {n : Nat} {k : Nat} (h : n 0) :
k Nat.log2 n 2 ^ k n
theorem Nat.log2_lt {n : Nat} {k : Nat} (h : n 0) :
Nat.log2 n < k n < 2 ^ k
theorem Nat.log2_self_le {n : Nat} (h : n 0) :
2 ^ Nat.log2 n n
theorem Nat.lt_log2_self {n : Nat} (h : n 0) :
n < 2 ^ (Nat.log2 n + 1)

sum #

@[simp]
theorem Nat.sum_nil :
Nat.sum [] = 0
@[simp]
theorem Nat.sum_cons {a : Nat} {l : List Nat} :
Nat.sum (a :: l) = a + Nat.sum l
@[simp]
theorem Nat.sum_append {l₁ : List Nat} {l₂ : List Nat} :
Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂