rewrite [← mul_transpose_eq_swap, sign_mul, sign_transpos i j h]
m n : Nat
x : Permutation n
i j : Fin n
h : i ≠ j
⊢ sign (swap x i j) = !sign x
m n : Nat
x : Permutation n
i j : Fin n
h : i ≠ j
⊢ (sign x != true) = !sign x