m n : ℕ
⊢ ↑(m / 2 ^ n) = ↑m / ↑(2 ^ n)
m n : ℕ
⊢ shiftr ↑m ↑n = ↑m / ↑(2 ^ n)
rw [shiftr_coe_nat, Nat.shiftr_eq_div_pow _ _]
no goals
m n : ℕ
⊢ ↑(m / 2 ^ n) = ↑m / ↑(2 ^ n)
simp
m n : ℕ
⊢ -[m / 2 ^ n+1] = -(div ↑m ↑(2 ^ n) + 1)

case H
m n : ℕ
⊢ 0 < ↑(2 ^ n)
m n : ℕ
⊢ shiftr -[m+1] ↑n = -[m+1] / ↑(2 ^ n)
rw [shiftr_negSucc, negSucc_ediv, Nat.shiftr_eq_div_pow]
case H
m n : ℕ
⊢ 0 < ↑(2 ^ n)
m n : ℕ
⊢ -[m / 2 ^ n+1] = -(div ↑m ↑(2 ^ n) + 1)

case H
m n : ℕ
⊢ 0 < ↑(2 ^ n)
rfl
no goals
case H
m n : ℕ
⊢ 0 < ↑(2 ^ n)
exact ofNat_lt_ofNat_of_lt (pow_pos (by decide) _)
no goals
m n : ℕ
⊢ 0 < 2
decide