clear this
m n : Nat
x y : Permutation n
this : (inversionNum x % 2 + inversionNum y % 2) % 2 = inversionNum (x * y) % 2
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))
m n : Nat
x y : Permutation n
⊢ ((inversionNum x % 2 + inversionNum y % 2) % 2 == 1) = ((inversionNum x % 2 == 1) != (inversionNum y % 2 == 1))