cases m.mod_two_eq_zero_or_one <;> cases n.mod_two_eq_zero_or_one
<;> rw [‹m%2=_›, ‹n%2=_›] <;> intro hdec <;> cases hdec <;> rfl
m n : Nat
⊢ decide (m % 2 = 1) = decide (n % 2 = 1) → m % 2 = n % 2
no goals