generalize y.inversionNum = n
m✝ n : Nat
x y : Permutation n
m : Nat
⊢ ((m % 2 + inversionNum y % 2) % 2 == 1) = ((m % 2 == 1) != (inversionNum y % 2 == 1))
m✝ n✝ : Nat
x y : Permutation n✝
m n : Nat
⊢ ((m % 2 + n % 2) % 2 == 1) = ((m % 2 == 1) != (n % 2 == 1))