case pos hn =>
  cases hn
  unfold bitwise; simp; simp [if_neg hm]
  cases hftf : f true false <;> by_cases hm2 : m / 2 = 0 <;> simp [hftf, hm2]
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
hn : n = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
no goals