conv => lhs; unfold bitwise; simp [if_neg hm, if_neg hn]
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : ¬n = 0
⊢ (if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then bitwise f (m / 2) (n / 2) + bitwise f (m / 2) (n / 2) + 1
      else bitwise f (m / 2) (n / 2) + bitwise f (m / 2) (n / 2)) /
      2 =
    bitwise f (m / 2) (n / 2)