cases m.mod_two_eq_zero_or_one
  <;> cases n.mod_two_eq_zero_or_one
  <;> rename_i hm hn
  <;> simp only [hm, hn]
m✝ n✝ : Nat
x y : Permutation n✝
m n : Nat
⊢ ((m % 2 + n % 2) % 2 == 1) = ((m % 2 == 1) != (n % 2 == 1))
no goals