apply m.mod_two_eq_zero_or_one.elim <;> apply n.mod_two_eq_zero_or_one.elim
<;> (intro hn hm; rw [hn, hm]; decide)
case h
m n : Nat
⊢ (m % 2 + n % 2) / 2 = if (decide (m % 2 = 1) && decide (n % 2 = 1)) = true then 1 else 0
no goals