have : (m &&& n).getBit 0 = false := by simp [disjoint]
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) / 2 = (m ^^^ n) / 2
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
this : getBit (m &&& n) 0 = false
⊢ (m + n) / 2 = (m ^^^ n) / 2