. show sign (x.inv ^ (k+1 : Nat)) = false
  apply sign_powNat_of_even
  rewrite [x.sign_inv]
  exact h
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (x ^ Int.negSucc k) = false
no goals