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