theorem Int.shiftRight_eq (n : Int) (s : Nat) : n >>> s = n.shiftRight s

@[simp]

theorem Int.natCast_shiftRight (n s : Nat) : ↑(n >>> s) = ↑n >>> s

@[simp]

theorem Int.negSucc_shiftRight (m n : Nat) : negSucc m >>> n = negSucc (m >>> n)

theorem Int.shiftRight_add (i : Int) (m n : Nat) : i >>> (m + n) = i >>> m >>> n

theorem Int.shiftRight_eq_div_pow (m : Int) (n : Nat) : m >>> n = m / ↑(2 ^ n)

@[simp]

theorem Int.zero_shiftRight (n : Nat) : 0 >>> n = 0

@[simp]

theorem Int.shiftRight_zero (n : Int) : n >>> 0 = n

theorem Int.le_shiftRight_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : n ≤ n >>> s

theorem Int.shiftRight_le_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) : n >>> s ≤ n

theorem Int.le_shiftRight_of_nonneg {n : Int} {s : Nat} (h : 0 ≤ n) : 0 ≤ n >>> s

theorem Int.shiftRight_le_of_nonpos {n : Int} {s : Nat} (h : n ≤ 0) : n >>> s ≤ 0

@[simp]

theorem Int.natCast_shiftLeft (n s : Nat) : ↑(n <<< s) = ↑n <<< s

@[simp]

theorem Int.zero_shiftLeft (n : Nat) : 0 <<< n = 0

@[simp]

theorem Int.shiftLeft_zero (n : Int) : n <<< 0 = n

theorem Int.shiftLeft_succ (m : Int) (n : Nat) : m <<< (n + 1) = m <<< n * 2

theorem Int.shiftLeft_succ' (m : Int) (n : Nat) : m <<< (n + 1) = 2 * m <<< n

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

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

theorem Int.shiftLeft_add (a : Int) (b c : Nat) : a <<< (b + c) = a <<< b <<< c

@[simp]

theorem Int.shiftLeft_shiftRight_cancel (a : Int) (b : Nat) : a <<< b >>> b = a

theorem Int.shiftLeft_shiftRight_eq_shiftLeft_of_le {b c : Nat} (h : c ≤ b) (a : Int) : a <<< b >>> c = a <<< (b - c)

theorem Int.shiftLeft_shiftRight_eq_shiftRight_of_le {b c : Nat} (h : b ≤ c) (a : Int) : a <<< b >>> c = a >>> (c - b)

theorem Int.shiftLeft_shiftRight_eq (a : Int) (b c : Nat) : a <<< b >>> c = a <<< (b - c) >>> (c - b)

@[simp]

theorem Int.shiftRight_shiftLeft_cancel {a : Int} {b : Nat} (h : 2 ^ b ∣ a) : a >>> b <<< b = a

theorem Int.add_shiftLeft (a b : Int) (n : Nat) : (a + b) <<< n = a <<< n + b <<< n

theorem Int.neg_shiftLeft (a : Int) (n : Nat) : (-a) <<< n = -a <<< n

theorem Int.shiftLeft_mul (a b : Int) (n : Nat) : a <<< n * b = (a * b) <<< n

theorem Int.mul_shiftLeft (a b : Int) (n : Nat) : a * b <<< n = (a * b) <<< n

theorem Int.shiftLeft_mul_shiftLeft (a b : Int) (m n : Nat) : a <<< m * b <<< n = (a * b) <<< (m + n)

@[simp]

theorem Int.shiftLeft_eq_zero_iff {a : Int} {n : Nat} : a <<< n = 0 ↔ a = 0

instance Int.instNeZeroHShiftLeftNat {a : Int} {n : Nat} [NeZero a] : NeZero (a <<< n)