intro (n' : ℕ) (ih : x^n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0) (_ : x^(step 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
x : α
n : ℕ
⊢ ∀ (m : ℕ), (x ^ m ≃ 0 → x ≃ 0 ∧ m ≄ 0) → x ^ step m ≃ 0 → x ≃ 0 ∧ step m ≄ 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
x : α
n n' : ℕ
ih : x ^ n' ≃ 0 → x ≃ 0 ∧ n' ≄ 0
x✝ : x ^ step n' ≃ 0
⊢ x ≃ 0 ∧ step n' ≄ 0