ℕ facts

theorem Nat.add_sub_eq_sub_sub {m n k : ℕ} (nk : n ≤ k) : m + n - k = m - (k - n)

theorem Nat.add_sub_lt_left {m n k : ℕ} (m0 : m ≠ 0) : m + n - k < m ↔ n < k

theorem Nat.bit_div2_eq (n : ℕ) : bit n.bodd n.div2 = n

theorem Nat.bit_le_bit {a b : Bool} {m n : ℕ} (ab : a ≤ b) (mn : m ≤ n) : bit a m ≤ bit b n

@[simp]

theorem Nat.testBit_zero' {i : ℕ} : testBit 0 i = false

theorem Nat.testBit_zero_eq_bodd {n : ℕ} : n.testBit 0 = n.bodd

theorem Nat.div2_eq_shiftRight_one {n : ℕ} : n.div2 = n >>> 1

@[simp]

theorem Nat.testBit_div2 {n i : ℕ} : n.div2.testBit i = n.testBit (i + 1)

theorem Nat.le_of_testBit_le {m n : ℕ} (h : ∀ (i : ℕ), m.testBit i ≤ n.testBit i) : m ≤ n

theorem Nat.land_le_max {m n : ℕ} : m &&& n ≤ max m n

theorem Nat.bodd_sub {n k : ℕ} : (n - k).bodd = ((n.bodd ^^ k.bodd) && decide (k ≤ n))

theorem Nat.bodd_sub_one {n : ℕ} : (n - 1).bodd = decide (n ≠ 0 ∧ ¬n.bodd = true)

theorem Nat.bodd_two_pow {k : ℕ} : (2 ^ k).bodd = decide (k = 0)

@[simp]

theorem Nat.pow_div' {a m n : ℕ} (a0 : a ≠ 0) : a ^ (m + n) / a ^ n = a ^ m

@[simp]

theorem Nat.pow_dvd' {a m n : ℕ} : a ^ n ∣ a ^ (m + n)

@[simp]

theorem Nat.pow_mod' {a m n : ℕ} : a ^ (m + n) % a ^ n = 0

@[simp]

theorem Nat.two_pow_sub_one_div_two_pow {n k : ℕ} : (2 ^ n - 1) / 2 ^ k = 2 ^ (n - k) - 1

theorem Nat.land_eq_mod {n k : ℕ} : n &&& 2 ^ k - 1 = n % 2 ^ k

theorem Nat.add_lt_add' {a b c d : ℕ} (ac : a < c) (bd : b ≤ d) : a + b < c + d

theorem Nat.add_lt_add'' {a b c d : ℕ} (ac : a ≤ c) (bd : b < d) : a + b < c + d

theorem Nat.mod_mul_eq_mul_mod (a n : ℕ) : a * n % n ^ 2 = a % n * n

theorem Nat.div_mod_mul_add_mod_eq {a n : ℕ} : a / n % n * n + a % n = a % n ^ 2

theorem Nat.lor_eq_add {a b : ℕ} (h : ∀ (i : ℕ), a.testBit i = false ∨ b.testBit i = false) : a ||| b = a + b

@[simp]

theorem Nat.testBit_mul_two_pow' {n k i : ℕ} : (n * 2 ^ k).testBit i = decide (k ≤ i ∧ n.testBit (i - k) = true)

theorem Nat.mod_le' {n k : ℕ} (k0 : 0 < k) : n % k ≤ k - 1

theorem Nat.div_div {n a b : ℕ} : n / a / b = n / (a * b)

theorem Nat.add_mod_two_pow_disjoint {x y a b : ℕ} (ya : y < 2 ^ a) : x * 2 ^ a % 2 ^ b + y % 2 ^ b = (x * 2 ^ a + y) % 2 ^ b

A case where +, % commute

theorem Nat.div_eq_zero_of_lt {m n : ℕ} (h : m < n) : m / n = 0

theorem Nat.sub_le_sub {a b c d : ℕ} (ab : a ≤ c) (db : d ≤ b) : a - b ≤ c - d

theorem Nat.cast_div_le_div_add_one {𝕜 : Type} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [FloorSemiring 𝕜] {a b : ℕ} : ↑a / ↑b ≤ ↑(a / b) + 1

theorem Nat.sub_sub_assoc {a b c : ℕ} (h : c ≤ b) : a + c - b = a - (b - c)

theorem Nat.le_add_div_mul {n k : ℕ} (k0 : 0 < k) : n ≤ (n + k - 1) / k * k

theorem Nat.two_pow_ne_zero {n : ℕ} : 2 ^ n ≠ 0

Divide and shift with controllable rounding

def Nat.rdiv (n k : ℕ) (up : Bool) : ℕ

Divide, rounding up or down

Equations

• n.rdiv k up = (bif up then n + (k - 1) else n) / k

@[irreducible]

def Nat.shiftRightRound (n k : ℕ) (up : Bool) : ℕ

Shift right, rounding up or down

Equations

• n.shiftRightRound k up = (bif up then n + (1 <<< k - 1) else n) >>> k

theorem Nat.shiftRightRound_eq_rdiv (n k : ℕ) (up : Bool) : n.shiftRightRound k up = n.rdiv (2 ^ k) up

theorem Nat.rdiv_le {a b : ℕ} : ↑(a.rdiv b false) ≤ ↑a / ↑b

rdiv rounds down if desired

theorem Nat.le_rdiv {a b : ℕ} : ↑a / ↑b ≤ ↑(a.rdiv b true)

rdiv rounds up if desired

theorem Nat.rdiv_le_rdiv {a b : ℕ} {u0 u1 : Bool} (u01 : u0 ≤ u1) : a.rdiv b u0 ≤ a.rdiv b u1

@[simp]

theorem Nat.zero_rdiv {b : ℕ} {up : Bool} : rdiv 0 b up = 0

@[simp]

theorem Nat.rdiv_zero {a : ℕ} {up : Bool} : a.rdiv 0 up = 0

rdiv by 0 is 0

@[simp]

theorem Nat.rdiv_one {a : ℕ} {up : Bool} : a.rdiv 1 up = a

rdiv by 1 does nothing

theorem Nat.rdiv_lt {a b : ℕ} {up : Bool} : ↑(a.rdiv b up) < ↑a / ↑b + 1

rdiv never rounds up by much

theorem Nat.rdiv_le_of_le_mul {a b c : ℕ} {up : Bool} (h : a ≤ c * b) : a.rdiv b up ≤ c

Prove rdiv ≤ in terms of a multiplication inequality

theorem Nat.le_rdiv_of_mul_le {a b c : ℕ} {up : Bool} (b0 : 0 < b) (h : c * b ≤ a) : c ≤ a.rdiv b up

Prove ≤ rdiv in terms of a multiplication inequality

@[simp]

theorem Nat.log2_one : log2 1 = 0