no goals
m n k : ℕ
⊢ shiftr (↑m) (↑n + ↑k) = shiftr (shiftr ↑m ↑n) ↑k
rw [shiftr_coe_nat, shiftr_coe_nat, ← Int.ofNat_add, shiftr_coe_nat, Nat.shiftr_add]
no goals
m n k : ℕ
⊢ shiftr -[m+1] (↑n + ↑k) = shiftr (shiftr -[m+1] ↑n) ↑k
rw [shiftr_negSucc, shiftr_negSucc, ← Int.ofNat_add, shiftr_negSucc, Nat.shiftr_add]