intro n' (ih : (x * y)^n' ≃ x^n' * y^n')
ℕ : 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 y : α
n : ℕ
⊢ ∀ (m : ℕ), (x * y) ^ m ≃ x ^ m * y ^ m → (x * y) ^ step m ≃ x ^ step m * y ^ step m
ℕ : 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 y : α
n n' : ℕ
ih : (x * y) ^ n' ≃ x ^ n' * y ^ n'
⊢ (x * y) ^ step n' ≃ x ^ step n' * y ^ step n'