simp only [Nat.succ_add, powNat_succ]
case succ
n : Nat
x : Permutation n
l k : Nat
IH : x ^ (k + l) = x ^ k * x ^ l
⊢ x ^ (Nat.succ k + l) = x ^ Nat.succ k * x ^ l
case succ
n : Nat
x : Permutation n
l k : Nat
IH : x ^ (k + l) = x ^ k * x ^ l
⊢ x * x ^ (k + l) = x * x ^ k * x ^ l