conv =>
  lhs; rw [←m.div_add_mod 2, ←n.div_add_mod 2]
  rw [←Nat.add_assoc, Nat.add_assoc _ (m%2), Nat.add_comm (m%2), ←Nat.add_assoc]
  rw [←Nat.mul_add 2, Nat.add_assoc, Nat.mul_add_div_left (x:=2) (y:=m/2+n/2) (z:=m%2+n%2) (by decide)]
m n : Nat
⊢ (m + n) / 2 = m / 2 + n / 2 + if getBit (m &&& n) 0 = true then 1 else 0
m n : Nat
⊢ m / 2 + n / 2 + (m % 2 + n % 2) / 2 = m / 2 + n / 2 + if getBit (m &&& n) 0 = true then 1 else 0