rewrite [powNat_succ, sign_mul, h, IH]
case succ
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
IH : sign (x ^ k) = false
⊢ sign (x ^ Nat.succ k) = false
case succ
m n : Nat
x : Permutation n
h : sign x = false
k : Nat
IH : sign (x ^ k) = false
⊢ (false != false) = false