by_cases m = 0
f : Bool → Bool → Bool
m n : Nat
⊢ bitwise (flip f) m n = bitwise f n m
case pos
f : Bool → Bool → Bool
m n : Nat
h✝ : m = 0
⊢ bitwise (flip f) m n = bitwise f n m

case neg
f : Bool → Bool → Bool
m n : Nat
h✝ : ¬m = 0
⊢ bitwise (flip f) m n = bitwise f n m