. have : (m &&& n).getBit 0 = false := by simp [disjoint]
  conv => lhs; simp [add_div_two, this]; change (m >>> 1) + (n >>> 1)
  conv => rhs; change (m ^^^ n) >>> 1; rw [xor_shiftRight]
  have : m >>> 1 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
  exact add_eq_xor (m:=m >>> 1) (n:=n >>> 1) (by rw [←land_shiftRight, disjoint]; rfl)
case right.hdiv
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) / 2 = (m ^^^ n) / 2

case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2
case right.hmod
m n : Nat
disjoint : m &&& n = 0
hm : m > 0
⊢ (m + n) % 2 = (m ^^^ n) % 2