Documentation

Init.Data.Nat.Lemmas

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.

@[reducible, inline, deprecated Nat.and_forall_add_one]
abbrev Nat.and_forall_succ {p : NatProp} :
(p 0 ∀ (n : Nat), p (n + 1)) ∀ (n : Nat), p n
Equations
Instances For
    @[reducible, inline, deprecated Nat.or_exists_add_one]
    abbrev Nat.or_exists_succ {p : NatProp} :
    (p 0 ∃ (n : Nat), p (n + 1)) Exists p
    Equations
    Instances For
      @[simp]
      theorem Nat.exists_ne_zero {P : NatProp} :
      (∃ (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

      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 = n.succ
      theorem Nat.succ_eq_one_add (n : Nat) :
      n.succ = 1 + n
      theorem Nat.succ_add_eq_add_succ (a : Nat) (b : Nat) :
      a.succ + b = a + b.succ
      theorem Nat.eq_zero_of_add_eq_zero_right {n : Nat} {m : Nat} (h : n + m = 0) :
      n = 0
      @[simp]
      theorem Nat.add_eq_zero_iff {n : Nat} {m : Nat} :
      n + m = 0 n = 0 m = 0
      @[simp]
      theorem Nat.add_left_cancel_iff {m : Nat} {k : Nat} {n : Nat} :
      n + m = n + k m = k
      @[simp]
      theorem Nat.add_right_cancel_iff {m : Nat} {k : Nat} {n : Nat} :
      m + n = k + n m = k
      @[simp]
      theorem Nat.add_left_eq_self {a : Nat} {b : Nat} :
      a + b = b a = 0
      @[simp]
      theorem Nat.add_right_eq_self {a : Nat} {b : Nat} :
      a + b = a b = 0
      @[simp]
      theorem Nat.self_eq_add_right {a : Nat} {b : Nat} :
      a = a + b b = 0
      @[simp]
      theorem Nat.self_eq_add_left {a : Nat} {b : Nat} :
      a = b + a b = 0
      @[simp]
      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 + nk < m
      theorem Nat.lt_of_add_lt_add_left {k : Nat} {m : Nat} {n : Nat} :
      n + k < n + mk < m
      @[simp]
      theorem Nat.add_lt_add_iff_left {k : Nat} {n : Nat} {m : Nat} :
      k + n < k + m n < m
      @[simp]
      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.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 + n0 < k
      @[simp]
      theorem Nat.lt_add_right_iff_pos {n : Nat} {k : Nat} :
      n < n + k 0 < k
      @[simp]
      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 = n.pred
      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) :
      n.succ - m - k.succ = n - m - k
      theorem Nat.add_sub_sub_add_right (n : Nat) (m : Nat) (k : Nat) (l : Nat) :
      n + l - m - (k + l) = 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) :
      n.succ - 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
      theorem Nat.add_le_of_le_sub' {n : Nat} {k : Nat} {m : Nat} (h : m k) :
      n k - mm + n k
      theorem Nat.le_sub_of_add_le' {n : Nat} {k : Nat} {m : Nat} :
      m + n kn 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 kk - m k - nn 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
      @[reducible, inline]
      abbrev Nat.sub_lt_self {a : Nat} {b : Nat} (h₀ : 0 < a) (h₁ : a b) :
      b - a < b
      Equations
      Instances For
        theorem Nat.add_lt_of_lt_sub' {a : Nat} {b : Nat} {c : Nat} :
        b < c - aa + 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.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 < a.succ
        theorem Nat.sub_lt_add_one (a : Nat) (b : Nat) :
        a - b < a + 1
        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 x.succ y.succ = (min x y).succ
        @[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
        @[simp]
        theorem Nat.min_assoc (a : Nat) (b : Nat) (c : Nat) :
        min (min a b) c = min a (min b c)
        @[simp]
        theorem Nat.min_self_assoc {m : Nat} {n : Nat} :
        min m (min m n) = min m n
        @[simp]
        theorem Nat.min_self_assoc' {m : Nat} {n : Nat} :
        min n (min m n) = min n m
        @[simp]
        theorem Nat.min_add_left {a : Nat} {b : Nat} :
        min a (b + a) = a
        @[simp]
        theorem Nat.min_add_right {a : Nat} {b : Nat} :
        min a (a + b) = a
        @[simp]
        theorem Nat.add_left_min {a : Nat} {b : Nat} :
        min (b + a) a = a
        @[simp]
        theorem Nat.add_right_min {a : Nat} {b : Nat} :
        min (a + b) a = a
        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 x.succ y.succ = (max x y).succ
        theorem Nat.max_le_of_le_of_le {a : Nat} {b : Nat} {c : Nat} :
        a cb cmax 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)
        @[simp]
        theorem Nat.max_add_left {a : Nat} {b : Nat} :
        max a (b + a) = b + a
        @[simp]
        theorem Nat.max_add_right {a : Nat} {b : Nat} :
        max a (a + b) = a + b
        @[simp]
        theorem Nat.add_left_max {a : Nat} {b : Nat} :
        max (b + a) a = b + a
        @[simp]
        theorem Nat.add_right_max {a : Nat} {b : Nat} :
        max (a + b) a = a + b
        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 x.pred y.pred = (min x y).pred
        theorem Nat.pred_max_pred (x : Nat) (y : Nat) :
        max x.pred y.pred = (max x y).pred
        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
        theorem Nat.sub_min_sub_left (a : Nat) (b : Nat) (c : Nat) :
        min (a - b) (a - c) = a - max b c
        theorem Nat.sub_max_sub_left (a : Nat) (b : Nat) (c : Nat) :
        max (a - b) (a - c) = a - min b c
        theorem Nat.mul_max_mul_right (a : Nat) (b : Nat) (c : Nat) :
        max (a * c) (b * c) = max a b * c
        theorem Nat.mul_min_mul_right (a : Nat) (b : Nat) (c : Nat) :
        min (a * c) (b * c) = min a b * c
        theorem Nat.mul_max_mul_left (a : Nat) (b : Nat) (c : Nat) :
        max (a * b) (a * c) = a * max b c
        theorem Nat.mul_min_mul_left (a : Nat) (b : Nat) (c : Nat) :
        min (a * b) (a * c) = a * min b c

        mul #

        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_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 0m 0n * 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) :
        a.succ * b.succ = a * b + a + b + 1
        theorem Nat.add_one_mul_add_one (a : Nat) (b : Nat) :
        (a + 1) * (b + 1) = 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) :
        a.succ * b.succ = 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.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 : 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
        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
        @[simp]
        theorem Nat.self_sub_mod (n : Nat) (k : Nat) [NeZero k] :
        (n - k) % n = n - k
        @[simp]
        theorem Nat.mod_mul_mod {a : Nat} {b : Nat} {c : Nat} :
        a % c * b % c = a * b % c

        pow #

        theorem Nat.pow_succ' {m : Nat} {n : Nat} :
        m ^ n.succ = m * m ^ n
        theorem Nat.pow_add_one' {m : Nat} {n : Nat} :
        m ^ (n + 1) = m * m ^ n
        @[simp]
        theorem Nat.pow_eq {m : Nat} {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
        @[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
        @[reducible, inline]
        abbrev Nat.pow_le_pow_left {n : Nat} {m : Nat} (h : n m) (i : Nat) :
        n ^ i m ^ i
        Equations
        Instances For
          @[reducible, inline]
          abbrev Nat.pow_le_pow_right {n : Nat} (hx : n > 0) {i : Nat} {j : Nat} :
          i jn ^ i n ^ j
          Equations
          Instances For
            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_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
            @[simp]
            theorem Nat.pow_pred_mul {x : Nat} {w : Nat} (h : 0 < w) :
            x ^ (w - 1) * x = x ^ w
            theorem Nat.pow_pred_lt_pow {x : Nat} {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 : Nat} {n : Nat} {m : Nat} (h : 1 < a) :
            a ^ n < a ^ m a ^ n * a a ^ m
            @[simp]
            theorem Nat.two_pow_pred_mul_two {w : Nat} (h : 0 < w) :
            2 ^ (w - 1) * 2 = 2 ^ w

            log2 #

            @[simp]
            theorem Nat.log2_zero :
            theorem Nat.le_log2 {n : Nat} {k : Nat} (h : n 0) :
            k n.log2 2 ^ k n
            theorem Nat.log2_lt {n : Nat} {k : Nat} (h : n 0) :
            n.log2 < k n < 2 ^ k
            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)

            dvd #

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

            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.shiftLeft_add (m : Nat) (n : Nat) (k : Nat) :
            m <<< (n + k) = m <<< n <<< k
            @[deprecated Nat.shiftLeft_add]
            theorem Nat.shiftLeft_shiftLeft (m : Nat) (n : Nat) (k : Nat) :
            m <<< n <<< k = m <<< (n + k)
            @[simp]
            theorem Nat.shiftLeft_shiftRight (x : Nat) (n : Nat) :
            x <<< n >>> n = x
            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 < nProp) [(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
            instance Nat.decidableForallFin {n : Nat} (P : Fin nProp) [DecidablePred P] :
            Decidable (∀ (i : Fin n), P i)
            Equations
            instance Nat.decidableBallLE (n : Nat) (P : (k : Nat) → k nProp) [(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
            instance Nat.decidableExistsLT {p : NatProp} [h : DecidablePred p] :
            DecidablePred fun (n : Nat) => ∃ (m : Nat), m < n p m
            Equations
            instance Nat.decidableExistsLE {p : NatProp} [DecidablePred p] :
            DecidablePred fun (n : Nat) => ∃ (m : Nat), m n p m
            Equations