calc
  _ ≃ x^n         := Rel.refl
  _ ≃ x^(step n') := pow_substR (Rel.symm ‹step n' ≃ n›)
  _ ≃ x^n' * x    := pow_step
  _ ≃ x^n' * 0    := AA.substR ‹x ≃ 0›
  _ ≃ 0           := AA.absorbR
ℕ : 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
this : Positive n
n' : ℕ
h✝ : step n' ≃ n
⊢ x ^ n ≃ 0
no goals