apply sign_powNat_of_even
case negSucc
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x ^ (k + 1)) = false
case negSucc.h
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
⊢ sign (inv x) = false