intro (And.intro (_ : x ≃ 0) (_ : n ≄ 0))
ℕ : 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✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
⊢ x ≃ 0 ∧ n ≄ 0 → x ^ n ≃ 0
ℕ : 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✝³ : OfNat α 0
inst✝² : AP (1 ≄ 0)
inst✝¹ : AA.ZeroProduct fun x x_1 => x * x_1
inst✝ : AA.Absorbing 0 fun x x_1 => x * x_1
x : α
n : ℕ
left✝ : x ≃ 0
right✝ : n ≄ 0
⊢ x ^ n ≃ 0