calc
  _ ≃ x^(step n' + m)   := Rel.refl
  _ ≃ x^(step (n' + m)) := pow_substR (Rel.symm AA.scompatL)
  _ ≃ x^(n' + m) * x    := pow_step
  _ ≃ (x^n' * x^m) * x  := AA.substL ih
  _ ≃ x^n' * (x^m * x)  := AA.assoc
  _ ≃ x^n' * (x * x^m)  := AA.substR AA.comm
  _ ≃ (x^n' * x) * x^m  := Rel.symm AA.assoc
  _ ≃ x^(step n') * x^m := AA.substL (Rel.symm pow_step)
ℕ : Type
inst✝¹¹ : Core ℕ
inst✝¹⁰ : Induction ℕ
inst✝⁹ : Addition ℕ
inst✝⁸ : Sign ℕ
inst✝⁷ : Multiplication ℕ
α : Type
mul : α → α → α
inst✝⁶ : EqvOp α
inst✝⁵ : OfNat α 1
inst✝⁴ : Exponentiation ℕ mul
inst✝³ : AA.Substitutive₂ (fun x x_1 => x * x_1) AA.tc (fun x x_1 => x ≃ x_1) fun x x_1 => x ≃ x_1
inst✝² : AA.Associative fun x x_1 => x * x_1
inst✝¹ : AA.Commutative fun x x_1 => x * x_1
inst✝ : AA.Identity 1 fun x x_1 => x * x_1
x : α
n m n' : ℕ
ih : x ^ (n' + m) ≃ x ^ n' * x ^ m
⊢ x ^ (step n' + m) ≃ x ^ step n' * x ^ m
no goals