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)
m n : Nat
⊢ decide ((m % 2 + n % 2) % 2 = 1) = (decide (m % 2 = 1) != decide (n % 2 = 1))
no goals