by_cases m = 0
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
⊢ bitwise f m n % 2 = if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0
case pos
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
h✝ : m = 0
⊢ bitwise f m n % 2 = if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0

case neg
f : Bool → Bool → Bool
f_stable : f false false = false
m n : Nat
h✝ : ¬m = 0
⊢ bitwise f m n % 2 = if f (decide (m % 2 = 1)) (decide (n % 2 = 1)) = true then 1 else 0