rw [←land_shiftRight, disjoint]
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ m >>> 1 &&& n >>> 1 = 0
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this✝ : getBit (m &&& n) 0 = false
this : m >>> 1 < m
⊢ 0 >>> 1 = 0