induction k with
| zero =>
  simp only [Nat.zero_eq, Nat.zero_add, powNat_zero, one_mul]
| succ k IH =>
  simp only [Nat.succ_add, powNat_succ]
  rw [mul_assoc, IH]
n : Nat
x : Permutation n
k l : Nat
⊢ x ^ (k + l) = x ^ k * x ^ l
no goals