simp [if_neg hm]
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ (if m = 0 then 0 else if f true false = true then m else 0) / 2 =
    if m / 2 = 0 then 0 else if f true false = true then m / 2 else 0
case refl
f : Bool → Bool → Bool
m : Nat
hm : ¬m = 0
⊢ (if f true false = true then m else 0) / 2 = if m / 2 = 0 then 0 else if f true false = true then m / 2 else 0