unfold getBit
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (getBit m 0 && getBit n 0) = true then 1 else 0
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0