apply m.mod_two_eq_zero_or_one.elim <;> intro h <;> simp [h]
f : Bool → Bool → Bool
f_stable : f false false = false
m : Nat
hm : ¬m = 0
hftf : f true false = true
this : ∀ (b : Bool), f b false = b
⊢ m % 2 = if m % 2 = 1 then 1 else 0
no goals