by_cases n = 0
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)
case pos
f : Bool → Bool → Bool
m n : Nat
hm : ¬m = 0
h✝ : n = 0
⊢ bitwise f m n / 2 = bitwise f (m / 2) (n / 2)

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