case neg hm =>
  unfold bitwise
  rw [if_neg hm, if_neg hm]
  dsimp
  have : m > 0 := Nat.pos_of_ne_zero hm
  have : m/2 < m := Nat.div_lt_self ‹m>0› (Nat.lt_succ_self 1)
  rw [bitwise_flip (m:=m/2) (n:=n/2)]
  rfl
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ bitwise (flip f) m n = bitwise f n m
no goals