have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (_ : a ≃ n - m)) :=
  Integer.as_diff a
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝² : Exponentiation ℚ
p₁ p₂ : ℚ
a : ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
⊢ p₁ ^ a ≃ p₂ ^ a
ℕ ℤ : Type
inst✝¹² : Natural ℕ
inst✝¹¹ : Integer ℤ
ℚ : Type
inst✝¹⁰ : Core ℚ
inst✝⁹ : Addition ℚ
inst✝⁸ : Multiplication ℚ
inst✝⁷ : Negation ℚ
inst✝⁶ : Reciprocation ℚ
inst✝⁵ : Division ℚ
inst✝⁴ : Sign ℚ
inst✝³ : Natural.Exponentiation ℕ fun x x_1 => x * x_1
inst✝² : Exponentiation ℚ
p₁ p₂ : ℚ
a : ℤ
inst✝¹ : AP (p₁ ≄ 0)
inst✝ : AP (p₂ ≄ 0)
x✝ : p₁ ≃ p₂
n m : ℕ
h✝ : a ≃ Coe.coe n - Coe.coe m
⊢ p₁ ^ a ≃ p₂ ^ a