conv at this =>
  simp only [sign_mul, sign_one]
  rewrite [Bool.bne_eq_false]
m n : Nat
x : Permutation n
this : sign (inv x * x) = sign 1
⊢ sign (inv x) = sign x
m n : Nat
x : Permutation n
this : sign (inv x) = sign x
⊢ sign (inv x) = sign x