have Exists.intro (n : ℕ) (Exists.intro (m : ℕ) (a_eqv : 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 q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
a : ℤ
⊢ (p * q) ^ a ≃ p ^ a * q ^ 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 q : ℚ
inst✝¹ : AP (p ≄ 0)
inst✝ : AP (q ≄ 0)
a : ℤ
n m : ℕ
a_eqv : a ≃ Coe.coe n - Coe.coe m
⊢ (p * q) ^ a ≃ p ^ a * q ^ a