cases hftf : f true false <;> by_cases hm2 : m / 2 = 0 <;> simp [hftf, hm2]
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
no goals