conv =>
  rhs; change if (bitwise and m n).getBit 0 = true then 1 else 0
  rw [bitwise_getBit and (by decide)]
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if getBit (m &&& n) 0 = true then 1 else 0
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (getBit m 0 && getBit n 0) = true then 1 else 0