case mpr =>
  intro (And.intro (_ : x ≃ 0) (_ : n ≄ 0))
  show x^n ≃ 0
  have : Positive n := Signed.positive_defn.mpr ‹n ≄ 0›
  have (Exists.intro (n' : ℕ) (_ : step n' ≃ n)) := positive_step this
  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 : ℕ
⊢ x ≃ 0 ∧ n ≄ 0 → x ^ n ≃ 0
no goals