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