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

@[simp]

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

@[simp]

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

theorem Int.shiftRight_add (i : Int) (m : Nat) (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