induction k with
| zero => rw [powNat_zero, sign_one]
| succ k IH =>
  rewrite [powNat_succ, sign_mul, h, IH]
  decide
m n : Nat
x : Permutation n
k : Nat
h : sign x = false
⊢ sign (x ^ k) = false
no goals