ink

theorem Nat.succ_ne_self (n : Nat) : Nat.succ n ≠ n

ink

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

ink

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

ink

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

ink

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

ink

theorem Nat.le_of_not_le {a : Nat} {b : Nat} : ¬a ≤ b → b ≤ a

ink

theorem Nat.pos_of_ne_zero {n : Nat} : n ≠ 0 → 0 < n

ink

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

ink

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

ink

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

ink

@[simp]

theorem Nat.not_le {a : Nat} {b : Nat} : ¬a ≤ b ↔ b < a

ink

@[simp]

theorem Nat.not_lt {a : Nat} {b : Nat} : ¬a < b ↔ b ≤ a

ink

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

ink

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

ink

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

ink

theorem Nat.add_le_add_iff_le_right (k : Nat) (n : Nat) (m : Nat) : n + k ≤ m + k ↔ n ≤ m

ink

theorem Nat.lt_of_add_lt_add_left {k : Nat} {n : Nat} {m : Nat} (h : k + n < k + m) : n < m

ink

theorem Nat.lt_of_add_lt_add_right {a : Nat} {b : Nat} {c : Nat} (h : a + b < c + b) : a < c

ink

theorem Nat.lt_add_right (a : Nat) (b : Nat) (c : Nat) (h : a < b) : a < b + c

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Nat.add_le_to_le_sub (x : Nat) {y : Nat} {k : Nat} (h : k ≤ y) : x + k ≤ y ↔ x ≤ y - k

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Nat.eq_zero_of_nonpos (n : Nat) : ¬0 < n → n = 0

ink

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

ink

theorem Nat.sub_eq_iff_eq_add {a : Nat} {b : Nat} {c : Nat} (ab : b ≤ a) : a - b = c ↔ a = c + b

ink

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

ink

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

ink

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

ink

theorem Nat.min_comm (a : Nat) (b : Nat) : min a b = min b a

ink

theorem Nat.min_le_right (a : Nat) (b : Nat) : min a b ≤ b

ink

theorem Nat.min_le_left (a : Nat) (b : Nat) : min a b ≤ a

ink

theorem Nat.le_min {a : Nat} {b : Nat} {c : Nat} : a ≤ min b c ↔ a ≤ b ∧ a ≤ c

ink

theorem Nat.min_eq_left {a : Nat} {b : Nat} (h : a ≤ b) : min a b = a

ink

theorem Nat.min_eq_right {a : Nat} {b : Nat} (h : b ≤ a) : min a b = b

ink

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

ink

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

ink

theorem Nat.max_comm (a : Nat) (b : Nat) : max a b = max b a

ink

theorem Nat.le_max_left (a : Nat) (b : Nat) : a ≤ max a b

ink

theorem Nat.le_max_right (a : Nat) (b : Nat) : b ≤ max a b

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Nat.succ_inj' {n : Nat} {m : Nat} : Nat.succ n = Nat.succ m ↔ n = m

ink

theorem Nat.succ_add_eq_succ_add (n : Nat) (m : Nat) : Nat.succ n + m = n + Nat.succ m

ink

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

ink

theorem Nat.eq_zero_of_add_eq_zero {n : Nat} {m : Nat} (H : n + m = 0) : n = 0 ∧ m = 0

ink

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

ink

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

ink

theorem Nat.mul_ne_zero {n : Nat} {m : Nat} (n0 : n ≠ 0) (m0 : m ≠ 0) : n * m ≠ 0

ink

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

ink

theorem Nat.le_lt_antisymm {n : Nat} {m : Nat} (h₁ : n ≤ m) (h₂ : m < n) : False

ink

theorem Nat.lt_le_antisymm {n : Nat} {m : Nat} (h₁ : n < m) (h₂ : m ≤ n) : False

ink

theorem Nat.lt_asymm {n : Nat} {m : Nat} (h₁ : n < m) : ¬m < n

ink

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

• Nat.lt_sum_ge a b = if h : a < b then PSum.inl h else PSum.inr (_ : b ≤ a)

ink

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.

ink

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

ink

theorem Nat.eq_or_lt_of_not_lt {a : Nat} {b : Nat} (hnlt : ¬a < b) : a = b ∨ b < a

ink

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

ink

theorem Nat.one_pos : 0 < 1

ink

theorem Nat.not_lt_of_le {n : Nat} {m : Nat} (h₁ : m ≤ n) : ¬n < m

ink

theorem Nat.not_le_of_lt {n : Nat} {m : Nat} : m < n → ¬n ≤ m

ink

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

ink

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

ink

theorem Nat.le_or_le (a : Nat) (b : Nat) : a ≤ b ∨ b ≤ a

ink

theorem Nat.lt_or_eq_of_le {n : Nat} {m : Nat} (h : n ≤ m) : n < m ∨ n = m

ink

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

ink

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

ink

theorem Nat.sub_add_eq_max {a : Nat} {b : Nat} : a - b + b = max a b

ink

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

ink

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

ink

theorem Nat.sub.right_comm (m : Nat) (n : Nat) (k : Nat) : m - n - k = m - k - n

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Nat.sub_lt_sub_left {k : Nat} {m : Nat} {n : Nat} : k < m → k < n → m - n < m - k

ink

theorem Nat.sub_lt_left_of_lt_add {n : Nat} {k : Nat} {m : Nat} (H : n ≤ k) (h : k < n + m) : k - n < m

ink

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

ink

theorem Nat.le_sub_iff_add_le {x : Nat} {y : Nat} {k : Nat} (h : k ≤ y) : x ≤ y - k ↔ x + k ≤ y

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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)

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

Equations

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

theorem Nat.mul_le_mul_of_nonneg_left {a : Nat} {b : Nat} {c : Nat} (h₁ : a ≤ b) : c * a ≤ c * b

ink

theorem Nat.mul_le_mul_of_nonneg_right {a : Nat} {b : Nat} {c : Nat} (h₁ : a ≤ b) : a * c ≤ b * c

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

log2

ink

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

ink

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

ink

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

ink

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

sum

ink

@[simp]

theorem Nat.sum_nil : Nat.sum [] = 0

ink

@[simp]

theorem Nat.sum_cons {a : Nat} {l : List Nat} : Nat.sum (a :: l) = a + Nat.sum l

ink

@[simp]

theorem Nat.sum_append {l₁ : List Nat} {l₂ : List Nat} : Nat.sum (l₁ ++ l₂) = Nat.sum l₁ + Nat.sum l₂